52 lines
1.0 KiB
Coq
52 lines
1.0 KiB
Coq
From HB Require Import structures.
|
|
From mathcomp Require Import all_ssreflect.
|
|
|
|
Inductive t: Type :=
|
|
| Zero: t
|
|
| One: t
|
|
| Add: t -> t -> t.
|
|
|
|
Fixpoint eqb (a b: t): bool :=
|
|
match a, b with
|
|
| Zero, Zero => true
|
|
| One, One => true
|
|
| Add x1 y1, Add x2 y2 => eqb x1 x2 && eqb y1 y2
|
|
| _, _ => false
|
|
end.
|
|
|
|
Section EqLemmas.
|
|
Lemma lm_eqb1 (a: t): a = a -> eqb a a.
|
|
Proof.
|
|
elim: a => //= a IHa b IHb H.
|
|
by rewrite IHa // IHb.
|
|
Qed.
|
|
|
|
Lemma lm_eqb2r (a b: t): a = b -> eqb a b.
|
|
Proof.
|
|
move <-.
|
|
by apply: lm_eqb1.
|
|
Qed.
|
|
|
|
Lemma lm_eqb2l (a b: t): eqb a b -> a = b.
|
|
Proof.
|
|
elim: a b => [||a IHa b IHb]; case => // x y /andP [H1 H2].
|
|
by rewrite (IHa x H1) (IHb y H2).
|
|
Qed.
|
|
|
|
Theorem eqP (a b: t): reflect (a=b) (eqb a b).
|
|
Proof.
|
|
apply (iffP idP).
|
|
- apply: lm_eqb2l.
|
|
- apply: lm_eqb2r.
|
|
Qed.
|
|
End EqLemmas.
|
|
|
|
HB.instance Definition _ := hasDecEq.Build t eqP.
|
|
|
|
HB.about t.
|
|
(*
|
|
HB: t is canonically equipped with structures:
|
|
- eqtype.Equality
|
|
(from "(stdin)", line 2)
|
|
*)
|