-ndefinition mcu_type_destruct :
- Πm1,m2:mcu_type.ΠP:Prop.m1 = m2 →
- match m1 with
- [ HC05 ⇒ match m2 with [ HC05 ⇒ P → P | _ ⇒ P ]
- | HC08 ⇒ match m2 with [ HC08 ⇒ P → P | _ ⇒ P ]
- | HCS08 ⇒ match m2 with [ HCS08 ⇒ P → P | _ ⇒ P ]
- | RS08 ⇒ match m2 with [ RS08 ⇒ P → P | _ ⇒ P ]
- ].
- #m1; #m2; #P;
- nelim m1;
- ##[ ##1: nelim m2; nnormalize; #H;
- ##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##2: nelim m2; nnormalize; #H;
- ##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##3: nelim m2; nnormalize; #H;
- ##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##4: nelim m2; nnormalize; #H;
- ##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
+nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
+ #m; #x1; #x2; #H;
+ nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #x1;
+ ncases op2;
+ #x2;
+ nchange with (eq_op x1 x2 = eq_op x2 x1);
+ nrewrite > (symmetric_eqop x1 x2);
+ napply refl_eq.
+nqed.
+
+nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #x1;
+ ncases op2;
+ #x2;
+ nchange with ((eq_op x1 x2 = true) → ?);
+ #H;
+ nrewrite > (eqop_to_eq … H);
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #p1;
+ ncases op2;
+ #p2; #H;
+ nrewrite > (anyop_destruct … H);
+ nchange with (eq_op p2 p2 = true);
+ nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
+ napply refl_eq.
+nqed.
+
+nlemma decidable_anyop : ∀m.∀x,y:any_opcode m.decidable (x = y).
+ #m; #x; nelim x; #e1; #y; nelim y; #e2;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_op e1 e2) …);
+ ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (anyop_destruct m … H1))
+ ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))