napply (λx.x).
nqed.
-nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
#e1; #e2;
nelim e1;
napply refl_eq.
nqed.
-nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
- #e1; #e2;
- ncases e1;
- ncases e2;
+nlemma eq_to_eqex : ∀n1,n2.n1 = n2 → eq_ex n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ napply refl_eq.
+nqed.
+
+nlemma neqex_to_neq : ∀n1,n2.eq_ex n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_ex n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqex n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
##]
nqed.
-nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
- #m1; #m2;
- ncases m1;
- ncases m2;
+nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (exadecim_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
##]
nqed.
-nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
- #x; #y;
- nnormalize;
- nelim x;
- nelim y;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
- nnormalize; #H;
- napply False_ind;
- napply (exadecim_destruct … H)
- ##]
+nlemma neq_to_neqex : ∀n1,n2.n1 ≠ n2 → eq_ex n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_ex n1 n2));
+ napply (not_to_not (eq_ex n1 n2 = true) (n1 = n2) ? H);
+ napply (eqex_to_eq n1 n2).
nqed.
-nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
+nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_ex x y = true) (eq_ex x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqex_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqex_to_neq … H))
##]
nqed.
-nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
+nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
#n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ex n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqex n1 n2 H);
+ napply (symmetric_eq ? (eq_ex n2 n1) false);
+ napply (neq_to_neqex n2 n1 (symmetric_neq ? n1 n2 H))
##]
nqed.