destruct H.
qed.
+lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true.
+ do 2 intro;
+ elim t1 0;
+ elim t2 0;
+ normalize;
+ intro;
+ try destruct H;
+ reflexivity.
+qed.
+
+definition eq_ast_type_aux ≝
+λT:Type.λf:T → T → bool.
+ let rec aux (nl1,nl2:ne_list T) on nl1 ≝
+ match nl1 with
+ [ ne_nil h ⇒ match nl2 with
+ [ ne_nil h' ⇒ f h h'
+ | ne_cons h' _ ⇒ false
+ ]
+ | ne_cons h t ⇒ match nl2 with
+ [ ne_nil h' ⇒ false
+ | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t')
+ ]
+ ] in aux.
+
let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
match t1 with
[ AST_TYPE_BASE bType1 ⇒ match t2 with
| AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
[ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
| AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
- [ AST_TYPE_STRUCT nelSubType2 ⇒
- fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
- [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
- [ None ⇒ pair ?? false (S (snd ?? t))
- | Some cfr ⇒ match eq_ast_type h cfr with
- [ true ⇒ pair ?? true (S (snd ?? t))
- | false ⇒ pair ?? false (S (snd ?? t)) ]]
- | false ⇒ t]) (pair ?? true O) nelSubType1)
+ [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2
| _ ⇒ false ]
].
-lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
- do 2 intro;
- cases t1; cases t2;
- [ 2,3,4,6,7,8: normalize; intro; destruct H
- | 1: change in ⊢ (? ? % ?→?) with (eq_ast_base_type a a1);
- intro;
- apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
- | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1));
- intro;
- cut (a = a1 ∧ n = n1);
- elim daemon.
- | 9: elim daemon
- ].
+lemma eq_ast_type_elim :
+ ∀P:ast_type → Prop.
+ (∀x.P (AST_TYPE_BASE x)) →
+ (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) →
+ (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) →
+ (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) →
+ (∀t.(P t)).
+ intros;
+ apply
+ (let rec aux t ≝
+ match t
+ return λt.P t
+ with
+ [ AST_TYPE_BASE b ⇒ H b
+ | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t)
+ | AST_TYPE_STRUCT l ⇒
+ let rec aux_l (l:ne_list ast_type ) ≝
+ match l
+ return λl.P (AST_TYPE_STRUCT l)
+ with
+ [ ne_nil t => H2 t (aux t)
+ | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl)
+ ] in aux_l l
+ ] in aux t);
qed.
-(* PERCHE' ??
- se in testa includo
- include "demo/natural_deduction.ma".
- la dimostrazione va fino in fondo ma poi impazzisce ast_tree.ma
- dicendo che la dichiarazione ast_id e' scorretta
-
- [ 1: alias id "And_elim_l" = "cic:/matita/demo/natural_deduction/And_elim_l.con".
- alias id "And_elim_r" = "cic:/matita/demo/natural_deduction/And_elim_r.con".
- apply (eq_f2 ??? (λx.λy.? x y) a a1 n n1 (And_elim_l ?? Hcut) (And_elim_r ?? Hcut))
- | 2: split;
- [ 2: apply (eqb_true_to_eq n n1 (andb_true_true_r ?? H))
- | 1: cut (eq_ast_Type a a1 = true);
- [ 2: apply (andb_true_true ?? H)
- | 1: TODO elim daemon
- ]
+lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: intros;
+ simplify in H;
+ rewrite > (eqastbasetype_to_eq ?? H);
+ reflexivity
+ | 2: simplify;
+ intros;
+ destruct H1
+ | 3: simplify;
+ intros;
+ destruct H1
+ | 4: simplify;
+ intros;
+ destruct H2
+ ]
+ | 2: intros 4;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ lapply (andb_true_true ?? H2) as H3;
+ lapply (andb_true_true_r ?? H2) as H4;
+ rewrite > (H ? H3);
+ rewrite > (eqb_true_to_eq ?? H4);
+ reflexivity
+ | 3: simplify;
+ intros;
+ destruct H2
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 3: intros 3;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ destruct H2
+ | 3: intros;
+ simplify in H2;
+ rewrite > (H x1);
+ [ reflexivity
+ | apply H2
]
+ | 4: intros;
+ simplify in H3;
+ destruct H3
]
- | 9: TODO elim daemon
- ]
+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify in H4;
+ lapply (andb_true_true ?? H4) as H5;
+ lapply (andb_true_true_r ?? H4) as H6;
+ rewrite > (H ? H5);
+ lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
+ destruct (K ?);
+ [ apply H6
+ | reflexivity
+ ]
+ ]
+ ].
+qed.
+
+lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H;
+ apply (eq_to_eqastbasetype x x (refl_eq ??))
+ | 2: simplify;
+ intros;
+ destruct H1
+ | 3: simplify;
+ intros;
+ destruct H1
+ | 4: simplify;
+ intros;
+ destruct H2
+ ]
+ | 2: intros 4;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H t (refl_eq ??));
+ rewrite > (eq_to_eqb_true n n (refl_eq ??));
+ reflexivity
+ | 3: simplify;
+ intros;
+ destruct H2
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 3: intros 3;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ destruct H2
+ | 3: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H x (refl_eq ??));
+ reflexivity
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify;
+ destruct H4;
+ rewrite > (H x (refl_eq ??));
+ rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
+ reflexivity
+ ]
+ ].
qed.
-*)
definition is_ast_base_type ≝
λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].