From: Ferruccio Guidi Date: Mon, 4 Sep 2006 19:03:44 +0000 (+0000) Subject: other working theorems + iso_trans axiomatized (proof saved in problems) X-Git-Tag: 0.4.95@7852~1080 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7cb659c0af2d665c649f87922be02eccde795542;p=helm.git other working theorems + iso_trans axiomatized (proof saved in problems) --- diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs.ma new file mode 100644 index 000000000..674b2a9e4 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs". + +include "T/defs.ma". + +inductive C: Set \def +| CSort: nat \to C +| CHead: C \to (K \to (T \to C)). + +definition cweight: + C \to nat +\def + let rec cweight (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O +| (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))]) in cweight. + +definition clt: + C \to (C \to Prop) +\def + \lambda (c1: C).(\lambda (c2: C).(lt (cweight c1) (cweight c2))). + +definition cle: + C \to (C \to Prop) +\def + \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))). + +definition CTail: + K \to (T \to (C \to C)) +\def + let rec CTail (k: K) (t: T) (c: C) on c: C \def (match c with [(CSort n) +\Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k +t d) h u)]) in CTail. + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/props.ma new file mode 100644 index 000000000..a9385d0a6 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/props.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/C/props". + +include "C/defs.ma". + +include "T/props.ma". + +theorem clt_cong: + \forall (c: C).(\forall (d: C).((clt c d) \to (\forall (k: K).(\forall (t: +T).(clt (CHead c k t) (CHead d k t)))))) +\def + \lambda (c: C).(\lambda (d: C).(\lambda (H: (lt (cweight c) (cweight +d))).(\lambda (_: K).(\lambda (t: T).(lt_le_S (plus (cweight c) (tweight t)) +(plus (cweight d) (tweight t)) (plus_lt_compat_r (cweight c) (cweight d) +(tweight t) H)))))). + +theorem clt_head: + \forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u)))) +\def + \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(eq_ind_r nat (plus (cweight +c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) (lt_le_S (plus +(cweight c) O) (plus (cweight c) (tweight u)) (plus_le_lt_compat (cweight c) +(cweight c) O (tweight u) (le_n (cweight c)) (tweight_lt u))) (cweight c) +(plus_n_O (cweight c))))). + +theorem clt_wf__q_ind: + \forall (P: ((C \to Prop))).(((\forall (n: nat).((\lambda (P: ((C \to +Prop))).(\lambda (n0: nat).(\forall (c: C).((eq nat (cweight c) n0) \to (P +c))))) P n))) \to (\forall (c: C).(P c))) +\def + let Q \def (\lambda (P: ((C \to Prop))).(\lambda (n: nat).(\forall (c: +C).((eq nat (cweight c) n) \to (P c))))) in (\lambda (P: ((C \to +Prop))).(\lambda (H: ((\forall (n: nat).(\forall (c: C).((eq nat (cweight c) +n) \to (P c)))))).(\lambda (c: C).(H (cweight c) c (refl_equal nat (cweight +c)))))). + +theorem clt_wf_ind: + \forall (P: ((C \to Prop))).(((\forall (c: C).(((\forall (d: C).((clt d c) +\to (P d)))) \to (P c)))) \to (\forall (c: C).(P c))) +\def + let Q \def (\lambda (P: ((C \to Prop))).(\lambda (n: nat).(\forall (c: +C).((eq nat (cweight c) n) \to (P c))))) in (\lambda (P: ((C \to +Prop))).(\lambda (H: ((\forall (c: C).(((\forall (d: C).((lt (cweight d) +(cweight c)) \to (P d)))) \to (P c))))).(\lambda (c: C).(clt_wf__q_ind +(\lambda (c0: C).(P c0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (c0: +C).(P c0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) +\to (Q (\lambda (c: C).(P c)) m))))).(\lambda (c0: C).(\lambda (H1: (eq nat +(cweight c0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: nat).(\forall +(m: nat).((lt m n) \to (\forall (c: C).((eq nat (cweight c) m) \to (P c)))))) +H0 (cweight c0) H1) in (H c0 (\lambda (d: C).(\lambda (H3: (lt (cweight d) +(cweight c0))).(H2 (cweight d) H3 d (refl_equal nat (cweight d))))))))))))) +c)))). + +theorem chead_ctail: + \forall (c: C).(\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: +K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c k t) (CTail h u d)))))))) +\def + \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (t: T).(\forall (k: K).(ex_3 +K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t) +(CTail h u d))))))))) (\lambda (n: nat).(\lambda (t: T).(\lambda (k: +K).(ex_3_intro K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C +(CHead (CSort n) k t) (CTail h u d))))) k (CSort n) t (refl_equal C (CHead +(CSort n) k t)))))) (\lambda (c0: C).(\lambda (H: ((\forall (t: T).(\forall +(k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C +(CHead c0 k t) (CTail h u d)))))))))).(\lambda (k: K).(\lambda (t: +T).(\lambda (t0: T).(\lambda (k0: K).(let H_x \def (H t k) in (let H0 \def +H_x in (ex_3_ind K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C +(CHead c0 k t) (CTail h u d))))) (ex_3 K C T (\lambda (h: K).(\lambda (d: +C).(\lambda (u: T).(eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)))))) +(\lambda (x0: K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H1: (eq C (CHead +c0 k t) (CTail x0 x2 x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c1: +C).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead +c1 k0 t0) (CTail h u d))))))) (ex_3_intro K C T (\lambda (h: K).(\lambda (d: +C).(\lambda (u: T).(eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail h u d))))) x0 +(CHead x1 k0 t0) x2 (refl_equal C (CHead (CTail x0 x2 x1) k0 t0))) (CHead c0 +k t) H1))))) H0))))))))) c). + +theorem clt_thead: + \forall (k: K).(\forall (u: T).(\forall (c: C).(clt c (CTail k u c)))) +\def + \lambda (k: K).(\lambda (u: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(clt +c0 (CTail k u c0))) (\lambda (n: nat).(clt_head k (CSort n) u)) (\lambda (c0: +C).(\lambda (H: (clt c0 (CTail k u c0))).(\lambda (k0: K).(\lambda (t: +T).(clt_cong c0 (CTail k u c0) H k0 t))))) c))). + +theorem c_tail_ind: + \forall (P: ((C \to Prop))).(((\forall (n: nat).(P (CSort n)))) \to +(((\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P (CTail k t +c))))))) \to (\forall (c: C).(P c)))) +\def + \lambda (P: ((C \to Prop))).(\lambda (H: ((\forall (n: nat).(P (CSort +n))))).(\lambda (H0: ((\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: +T).(P (CTail k t c)))))))).(\lambda (c: C).(clt_wf_ind (\lambda (c0: C).(P +c0)) (\lambda (c0: C).(match c0 in C return (\lambda (c1: C).(((\forall (d: +C).((clt d c1) \to (P d)))) \to (P c1))) with [(CSort n) \Rightarrow (\lambda +(_: ((\forall (d: C).((clt d (CSort n)) \to (P d))))).(H n)) | (CHead c1 k t) +\Rightarrow (\lambda (H1: ((\forall (d: C).((clt d (CHead c1 k t)) \to (P +d))))).(let H_x \def (chead_ctail c1 t k) in (let H2 \def H_x in (ex_3_ind K +C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c1 k t) +(CTail h u d))))) (P (CHead c1 k t)) (\lambda (x0: K).(\lambda (x1: +C).(\lambda (x2: T).(\lambda (H3: (eq C (CHead c1 k t) (CTail x0 x2 +x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c2: C).(P c2)) (let H4 \def +(eq_ind C (CHead c1 k t) (\lambda (c: C).(\forall (d: C).((clt d c) \to (P +d)))) H1 (CTail x0 x2 x1) H3) in (H0 x1 (H4 x1 (clt_thead x0 x2 x1)) x0 x2)) +(CHead c1 k t) H3))))) H2))))])) c)))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma index cf483de06..5db781439 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma @@ -47,7 +47,10 @@ definition THeads: T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u (THeads k ul t))])) in THeads. -inductive C: Set \def -| CSort: nat \to C -| CHead: C \to (K \to (T \to C)). +definition tweight: + T \to nat +\def + let rec tweight (t: T) on t: nat \def (match t with [(TSort _) \Rightarrow +(S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus +(tweight u) (tweight t0)))]) in tweight. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma index a9c293f20..95088bb19 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma @@ -67,3 +67,12 @@ v (\lambda (t: T).((eq T (THead k t t1) t1) \to (\forall (P: Prop).P))) H0 t0 H5) in (let H8 \def (eq_ind K k (\lambda (k: K).((eq T (THead k t0 t1) t1) \to (\forall (P: Prop).P))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))). +theorem tweight_lt: + \forall (t: T).(lt O (tweight t)) +\def + \lambda (t: T).(match t in T return (\lambda (t0: T).(lt O (tweight t0))) +with [(TSort _) \Rightarrow (le_n (S O)) | (TLRef _) \Rightarrow (le_n (S O)) +| (THead _ t0 t1) \Rightarrow (le_S_n (S O) (S (plus (tweight t0) (tweight +t1))) (le_n_S (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S O (plus +(tweight t0) (tweight t1)) (le_O_n (plus (tweight t0) (tweight t1))))))]). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma new file mode 100644 index 000000000..55d6153a8 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs". + +include "C/defs.ma". + +definition clen: + C \to nat +\def + let rec clen (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O | +(CHead c0 k _) \Rightarrow (s k (clen c0))]) in clen. + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs.ma new file mode 100644 index 000000000..ca224f0b3 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs". + +include "C/defs.ma". + +definition fweight: + C \to (T \to nat) +\def + \lambda (c: C).(\lambda (t: T).(plus (cweight c) (tweight t))). + +definition flt: + C \to (T \to (C \to (T \to Prop))) +\def + \lambda (c1: C).(\lambda (t1: T).(\lambda (c2: C).(\lambda (t2: T).(lt +(fweight c1 t1) (fweight c2 t2))))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma new file mode 100644 index 000000000..93edf9062 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma @@ -0,0 +1,129 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props". + +include "flt/defs.ma". + +include "C/props.ma". + +theorem flt_thead_sx: + \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c +(THead k u t))))) +\def + \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_le_S +(plus (cweight c) (tweight u)) (plus (cweight c) (S (plus (tweight u) +(tweight t)))) (plus_le_lt_compat (cweight c) (cweight c) (tweight u) (S +(plus (tweight u) (tweight t))) (le_n (cweight c)) (le_lt_n_Sm (tweight u) +(plus (tweight u) (tweight t)) (le_plus_l (tweight u) (tweight t)))))))). + +theorem flt_thead_dx: + \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c +(THead k u t))))) +\def + \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_le_S +(plus (cweight c) (tweight t)) (plus (cweight c) (S (plus (tweight u) +(tweight t)))) (plus_le_lt_compat (cweight c) (cweight c) (tweight t) (S +(plus (tweight u) (tweight t))) (le_n (cweight c)) (le_lt_n_Sm (tweight t) +(plus (tweight u) (tweight t)) (le_plus_r (tweight u) (tweight t)))))))). + +theorem flt_shift: + \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c +k u) t c (THead k u t))))) +\def + \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(eq_ind nat +(S (plus (cweight c) (plus (tweight u) (tweight t)))) (\lambda (n: nat).(lt +(plus (plus (cweight c) (tweight u)) (tweight t)) n)) (eq_ind_r nat (plus +(plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus +(cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight +c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight +t))) (plus_assoc (cweight c) (tweight u) (tweight t))) (plus (cweight c) (S +(plus (tweight u) (tweight t)))) (plus_n_Sm (cweight c) (plus (tweight u) +(tweight t))))))). + +theorem flt_arith0: + \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t +(CHead c k t) (TLRef i))))) +\def + \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: nat).(le_S_n (S +(plus (cweight c) (tweight t))) (plus (plus (cweight c) (tweight t)) (S O)) +(lt_le_S (S (plus (cweight c) (tweight t))) (S (plus (plus (cweight c) +(tweight t)) (S O))) (lt_n_S (plus (cweight c) (tweight t)) (plus (plus +(cweight c) (tweight t)) (S O)) (lt_x_plus_x_Sy (plus (cweight c) (tweight +t)) O))))))). + +theorem flt_arith1: + \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle +(CHead c1 k1 t1) c2) \to (\forall (k2: K).(\forall (t2: T).(\forall (i: +nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i))))))))) +\def + \lambda (_: K).(\lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda +(H: (le (plus (cweight c1) (tweight t1)) (cweight c2))).(\lambda (_: +K).(\lambda (t2: T).(\lambda (_: nat).(le_lt_trans (plus (cweight c1) +(tweight t1)) (cweight c2) (plus (plus (cweight c2) (tweight t2)) (S O)) H +(eq_ind_r nat (plus (S O) (plus (cweight c2) (tweight t2))) (\lambda (n: +nat).(lt (cweight c2) n)) (le_lt_n_Sm (cweight c2) (plus (cweight c2) +(tweight t2)) (le_plus_l (cweight c2) (tweight t2))) (plus (plus (cweight c2) +(tweight t2)) (S O)) (plus_comm (plus (cweight c2) (tweight t2)) (S +O))))))))))). + +theorem flt_arith2: + \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1 +t1 c2 (TLRef i)) \to (\forall (k2: K).(\forall (t2: T).(\forall (j: nat).(flt +c1 t1 (CHead c2 k2 t2) (TLRef j))))))))) +\def + \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (_: nat).(\lambda +(H: (lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)))).(\lambda +(_: K).(\lambda (t2: T).(\lambda (_: nat).(lt_le_trans (plus (cweight c1) +(tweight t1)) (plus (cweight c2) (S O)) (plus (plus (cweight c2) (tweight +t2)) (S O)) H (le_S_n (plus (cweight c2) (S O)) (plus (plus (cweight c2) +(tweight t2)) (S O)) (lt_le_S (plus (cweight c2) (S O)) (S (plus (plus +(cweight c2) (tweight t2)) (S O))) (le_lt_n_Sm (plus (cweight c2) (S O)) +(plus (plus (cweight c2) (tweight t2)) (S O)) (plus_le_compat (cweight c2) +(plus (cweight c2) (tweight t2)) (S O) (S O) (le_plus_l (cweight c2) (tweight +t2)) (le_n (S O)))))))))))))). + +theorem flt_wf__q_ind: + \forall (P: ((C \to (T \to Prop)))).(((\forall (n: nat).((\lambda (P: ((C +\to (T \to Prop)))).(\lambda (n0: nat).(\forall (c: C).(\forall (t: T).((eq +nat (fweight c t) n0) \to (P c t)))))) P n))) \to (\forall (c: C).(\forall +(t: T).(P c t)))) +\def + let Q \def (\lambda (P: ((C \to (T \to Prop)))).(\lambda (n: nat).(\forall +(c: C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t)))))) in (\lambda +(P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (n: nat).(\forall (c: +C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t))))))).(\lambda (c: +C).(\lambda (t: T).(H (fweight c t) c t (refl_equal nat (fweight c t))))))). + +theorem flt_wf_ind: + \forall (P: ((C \to (T \to Prop)))).(((\forall (c2: C).(\forall (t2: +T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) +\to (P c2 t2))))) \to (\forall (c: C).(\forall (t: T).(P c t)))) +\def + let Q \def (\lambda (P: ((C \to (T \to Prop)))).(\lambda (n: nat).(\forall +(c: C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t)))))) in (\lambda +(P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (c2: C).(\forall (t2: +T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) +\to (P c2 t2)))))).(\lambda (c: C).(\lambda (t: T).(flt_wf__q_ind P (\lambda +(n: nat).(lt_wf_ind n (Q P) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: +nat).((lt m n0) \to (Q P m))))).(\lambda (c0: C).(\lambda (t0: T).(\lambda +(H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: +nat).(\forall (m: nat).((lt m n) \to (\forall (c: C).(\forall (t: T).((eq nat +(fweight c t) m) \to (P c t))))))) H0 (fweight c0 t0) H1) in (H c0 t0 +(\lambda (c1: C).(\lambda (t1: T).(\lambda (H3: (flt c1 t1 c0 t0)).(H2 +(fweight c1 t1) H3 c1 t1 (refl_equal nat (fweight c1 t1))))))))))))))) c +t))))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma index 4823ffdbf..c6cd772d2 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma @@ -18,90 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props". include "iso/defs.ma". -theorem iso_trans: +axiom iso_trans: \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 t3) \to (iso t1 t3))))) -\def - \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda -(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3))))) -(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso -(TSort n2) t3)).(let H1 \def (match H0 in iso return (\lambda (t: T).(\lambda -(t0: T).(\lambda (_: (iso t t0)).((eq T t (TSort n2)) \to ((eq T t0 t3) \to -(iso (TSort n1) t3)))))) with [(iso_sort n0 n3) \Rightarrow (\lambda (H0: (eq -T (TSort n0) (TSort n2))).(\lambda (H1: (eq T (TSort n3) t3)).((let H2 \def -(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with -[(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) -\Rightarrow n0])) (TSort n0) (TSort n2) H0) in (eq_ind nat n2 (\lambda (_: -nat).((eq T (TSort n3) t3) \to (iso (TSort n1) t3))) (\lambda (H3: (eq T -(TSort n3) t3)).(eq_ind T (TSort n3) (\lambda (t: T).(iso (TSort n1) t)) -(iso_sort n1 n3) t3 H3)) n0 (sym_eq nat n0 n2 H2))) H1))) | (iso_lref i1 i2) -\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TSort n2))).(\lambda (H1: (eq T -(TLRef i2) t3)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e -in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef -_) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n2) H0) in -(False_ind ((eq T (TLRef i2) t3) \to (iso (TSort n1) t3)) H2)) H1))) | -(iso_head k v1 v2 t1 t2) \Rightarrow (\lambda (H0: (eq T (THead k v1 t1) -(TSort n2))).(\lambda (H1: (eq T (THead k v2 t2) t3)).((let H2 \def (eq_ind T -(THead k v1 t1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) -with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ -_) \Rightarrow True])) I (TSort n2) H0) in (False_ind ((eq T (THead k v2 t2) -t3) \to (iso (TSort n1) t3)) H2)) H1)))]) in (H1 (refl_equal T (TSort n2)) -(refl_equal T t3))))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3: -T).(\lambda (H0: (iso (TLRef i2) t3)).(let H1 \def (match H0 in iso return -(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (TLRef -i2)) \to ((eq T t0 t3) \to (iso (TLRef i1) t3)))))) with [(iso_sort n1 n2) -\Rightarrow (\lambda (H0: (eq T (TSort n1) (TLRef i2))).(\lambda (H1: (eq T -(TSort n2) t3)).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e -in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef -_) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i2) H0) in -(False_ind ((eq T (TSort n2) t3) \to (iso (TLRef i1) t3)) H2)) H1))) | -(iso_lref i0 i3) \Rightarrow (\lambda (H0: (eq T (TLRef i0) (TLRef -i2))).(\lambda (H1: (eq T (TLRef i3) t3)).((let H2 \def (f_equal T nat -(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) -\Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) -(TLRef i0) (TLRef i2) H0) in (eq_ind nat i2 (\lambda (_: nat).((eq T (TLRef -i3) t3) \to (iso (TLRef i1) t3))) (\lambda (H3: (eq T (TLRef i3) t3)).(eq_ind -T (TLRef i3) (\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 i3) t3 H3)) i0 -(sym_eq nat i0 i2 H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow (\lambda -(H0: (eq T (THead k v1 t1) (TLRef i2))).(\lambda (H1: (eq T (THead k v2 t2) -t3)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i2) H0) in -(False_ind ((eq T (THead k v2 t2) t3) \to (iso (TLRef i1) t3)) H2)) H1)))]) -in (H1 (refl_equal T (TLRef i2)) (refl_equal T t3))))))) (\lambda (k: -K).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: -T).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H1 \def -(match H0 in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t -t0)).((eq T t (THead k v2 t4)) \to ((eq T t0 t5) \to (iso (THead k v1 t3) -t5)))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1) -(THead k v2 t4))).(\lambda (H1: (eq T (TSort n2) t5)).((let H2 \def (eq_ind T -(TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with -[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) -\Rightarrow False])) I (THead k v2 t4) H0) in (False_ind ((eq T (TSort n2) -t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) | (iso_lref i1 i2) \Rightarrow -(\lambda (H0: (eq T (TLRef i1) (THead k v2 t4))).(\lambda (H1: (eq T (TLRef -i2) t5)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k v2 t4) H0) -in (False_ind ((eq T (TLRef i2) t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) -| (iso_head k0 v0 v3 t0 t4) \Rightarrow (\lambda (H0: (eq T (THead k0 v0 t0) -(THead k v2 t4))).(\lambda (H1: (eq T (THead k0 v3 t4) t5)).((let H2 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with -[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) -\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H3 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with -[(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _) -\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H4 \def -(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with -[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k _ _) -\Rightarrow k])) (THead k0 v0 t0) (THead k v2 t4) H0) in (eq_ind K k (\lambda -(k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t4) t5) \to -(iso (THead k v1 t3) t5))))) (\lambda (H5: (eq T v0 v2)).(eq_ind T v2 -(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t4) t5) \to (iso (THead -k v1 t3) t5)))) (\lambda (H6: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq -T (THead k v3 t4) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H7: (eq T -(THead k v3 t4) t5)).(eq_ind T (THead k v3 t4) (\lambda (t: T).(iso (THead k -v1 t3) t)) (iso_head k v1 v3 t3 t4) t5 H7)) t0 (sym_eq T t0 t4 H6))) v0 -(sym_eq T v0 v2 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H1 -(refl_equal T (THead k v2 t4)) (refl_equal T t5)))))))))) t1 t2 H))). +. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma index de2399b05..995eeae40 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma @@ -25,6 +25,94 @@ include "LambdaDelta/theory.ma". iso_trans (in iso/props) +theorem iso_trans: + \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 +t3) \to (iso t1 t3))))) +\def + \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda +(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3))))) +(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso +(TSort n2) t3)).(let H1 \def (match H0 in iso return (\lambda (t: T).(\lambda +(t0: T).(\lambda (_: (iso t t0)).((eq T t (TSort n2)) \to ((eq T t0 t3) \to +(iso (TSort n1) t3)))))) with [(iso_sort n0 n3) \Rightarrow (\lambda (H0: (eq +T (TSort n0) (TSort n2))).(\lambda (H1: (eq T (TSort n3) t3)).((let H2 \def +(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with +[(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) +\Rightarrow n0])) (TSort n0) (TSort n2) H0) in (eq_ind nat n2 (\lambda (_: +nat).((eq T (TSort n3) t3) \to (iso (TSort n1) t3))) (\lambda (H3: (eq T +(TSort n3) t3)).(eq_ind T (TSort n3) (\lambda (t: T).(iso (TSort n1) t)) +(iso_sort n1 n3) t3 H3)) n0 (sym_eq nat n0 n2 H2))) H1))) | (iso_lref i1 i2) +\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TSort n2))).(\lambda (H1: (eq T +(TLRef i2) t3)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e +in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef +_) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n2) H0) in +(False_ind ((eq T (TLRef i2) t3) \to (iso (TSort n1) t3)) H2)) H1))) | +(iso_head k v1 v2 t1 t2) \Rightarrow (\lambda (H0: (eq T (THead k v1 t1) +(TSort n2))).(\lambda (H1: (eq T (THead k v2 t2) t3)).((let H2 \def (eq_ind T +(THead k v1 t1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) +with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ +_) \Rightarrow True])) I (TSort n2) H0) in (False_ind ((eq T (THead k v2 t2) +t3) \to (iso (TSort n1) t3)) H2)) H1)))]) in (H1 (refl_equal T (TSort n2)) +(refl_equal T t3))))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3: +T).(\lambda (H0: (iso (TLRef i2) t3)).(let H1 \def (match H0 in iso return +(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (TLRef +i2)) \to ((eq T t0 t3) \to (iso (TLRef i1) t3)))))) with [(iso_sort n1 n2) +\Rightarrow (\lambda (H0: (eq T (TSort n1) (TLRef i2))).(\lambda (H1: (eq T +(TSort n2) t3)).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e +in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef +_) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i2) H0) in +(False_ind ((eq T (TSort n2) t3) \to (iso (TLRef i1) t3)) H2)) H1))) | +(iso_lref i0 i3) \Rightarrow (\lambda (H0: (eq T (TLRef i0) (TLRef +i2))).(\lambda (H1: (eq T (TLRef i3) t3)).((let H2 \def (f_equal T nat +(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) +\Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) +(TLRef i0) (TLRef i2) H0) in (eq_ind nat i2 (\lambda (_: nat).((eq T (TLRef +i3) t3) \to (iso (TLRef i1) t3))) (\lambda (H3: (eq T (TLRef i3) t3)).(eq_ind +T (TLRef i3) (\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 i3) t3 H3)) i0 +(sym_eq nat i0 i2 H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow (\lambda +(H0: (eq T (THead k v1 t1) (TLRef i2))).(\lambda (H1: (eq T (THead k v2 t2) +t3)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T +return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i2) H0) in +(False_ind ((eq T (THead k v2 t2) t3) \to (iso (TLRef i1) t3)) H2)) H1)))]) +in (H1 (refl_equal T (TLRef i2)) (refl_equal T t3))))))) (\lambda (k: +K).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: +T).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H1 \def +(match H0 in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t +t0)).((eq T t (THead k v2 t4)) \to ((eq T t0 t5) \to (iso (THead k v1 t3) +t5)))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1) +(THead k v2 t4))).(\lambda (H1: (eq T (TSort n2) t5)).((let H2 \def (eq_ind T +(TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with +[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) +\Rightarrow False])) I (THead k v2 t4) H0) in (False_ind ((eq T (TSort n2) +t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) | (iso_lref i1 i2) \Rightarrow +(\lambda (H0: (eq T (TLRef i1) (THead k v2 t4))).(\lambda (H1: (eq T (TLRef +i2) t5)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T +return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k v2 t4) H0) +in (False_ind ((eq T (TLRef i2) t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) +| (iso_head k0 v0 v3 t0 t4) \Rightarrow (\lambda (H0: (eq T (THead k0 v0 t0) +(THead k v2 t4))).(\lambda (H1: (eq T (THead k0 v3 t4) t5)).((let H2 \def +(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) +\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H3 \def +(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +[(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _) +\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H4 \def +(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with +[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k _ _) +\Rightarrow k])) (THead k0 v0 t0) (THead k v2 t4) H0) in (eq_ind K k (\lambda +(k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t4) t5) \to +(iso (THead k v1 t3) t5))))) (\lambda (H5: (eq T v0 v2)).(eq_ind T v2 +(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t4) t5) \to (iso (THead +k v1 t3) t5)))) (\lambda (H6: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq +T (THead k v3 t4) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H7: (eq T +(THead k v3 t4) t5)).(eq_ind T (THead k v3 t4) (\lambda (t: T).(iso (THead k +v1 t3) t)) (iso_head k v1 v3 t3 t4) t5 H7)) t0 (sym_eq T t0 t4 H6))) v0 +(sym_eq T v0 v2 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H1 +(refl_equal T (THead k v2 t4)) (refl_equal T t5)))))))))) t1 t2 H))). + + drop1_getl_trans (* Problem 1: does not typecheck a match on an empty type *)