From f764844fa35ab0bb9c10707151340b924060f069 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Sep 2006 15:34:18 +0000 Subject: [PATCH] firs error: iso/props --- .../Level-1/LambdaDelta/T/defs.ma | 4 + .../Level-1/LambdaDelta/iso/defs.ma | 26 ++ .../Level-1/LambdaDelta/iso/fwd.ma | 203 ++++++++++++ .../Level-1/LambdaDelta/iso/props.ma | 107 +++++++ .../Level-1/LambdaDelta/r/defs.ma | 26 ++ .../Level-1/LambdaDelta/r/props.ma | 96 ++++++ .../Level-1/LambdaDelta/tlt/defs.ma | 48 +++ .../Level-1/LambdaDelta/tlt/props.ma | 302 ++++++++++++++++++ .../contribs/LAMBDA-TYPES/Level-1/problems.ma | 12 +- 9 files changed, 819 insertions(+), 5 deletions(-) create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma 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 42d3dcb19..cf483de06 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma @@ -47,3 +47,7 @@ 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)). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma new file mode 100644 index 000000000..cf815b7bc --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/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/iso/defs". + +include "T/defs.ma". + +inductive iso: T \to (T \to Prop) \def +| iso_sort: \forall (n1: nat).(\forall (n2: nat).(iso (TSort n1) (TSort n2))) +| iso_lref: \forall (i1: nat).(\forall (i2: nat).(iso (TLRef i1) (TLRef i2))) +| iso_head: \forall (k: K).(\forall (v1: T).(\forall (v2: T).(\forall (t1: +T).(\forall (t2: T).(iso (THead k v1 t1) (THead k v2 t2)))))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma new file mode 100644 index 000000000..526a3f603 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma @@ -0,0 +1,203 @@ +(**************************************************************************) +(* ___ *) +(* ||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/iso/fwd". + +include "iso/defs.ma". + +theorem iso_flats_lref_bind_false: + \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall +(t: T).(\forall (vs: TList).((iso (THeads (Flat f) vs (TLRef i)) (THead (Bind +b) v t)) \to (\forall (P: Prop).P))))))) +\def + \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda +(t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads +(Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P))) +(\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 +\def (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: +(iso t0 t1)).((eq T t0 (TLRef i)) \to ((eq T t1 (THead (Bind b) v t)) \to +P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1) +(TLRef i))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v t))).((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 i) H0) in (False_ind ((eq T +(TSort n2) (THead (Bind b) v t)) \to P) H2)) H1))) | (iso_lref i1 i2) +\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef i))).(\lambda (H1: (eq T +(TLRef i2) (THead (Bind b) v t))).((let H2 \def (f_equal T nat (\lambda (e: +T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i1 | +(TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) (TLRef i1) (TLRef +i) H0) in (eq_ind nat i (\lambda (_: nat).((eq T (TLRef i2) (THead (Bind b) v +t)) \to P)) (\lambda (H3: (eq T (TLRef i2) (THead (Bind b) v t))).(let H4 +\def (eq_ind T (TLRef i2) (\lambda (e: T).(match e in T return (\lambda (_: +T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | +(THead _ _ _) \Rightarrow False])) I (THead (Bind b) v t) H3) in (False_ind P +H4))) i1 (sym_eq nat i1 i H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow +(\lambda (H0: (eq T (THead k v1 t1) (TLRef i))).(\lambda (H1: (eq T (THead k +v2 t2) (THead (Bind b) v t))).((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 i) H0) in (False_ind ((eq T (THead k v2 t2) (THead (Bind b) +v t)) \to P) H2)) H1)))]) in (H0 (refl_equal T (TLRef i)) (refl_equal T +(THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: +(((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: +Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef +i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H1 \def (match H0 in iso +return (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (iso t2 t3)).((eq T t2 +(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) \to ((eq T t3 (THead +(Bind b) v t)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: +(eq T (TSort n1) (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef +i))))).(\lambda (H2: (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \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 (Flat f) t0 (THeads (Flat f) t1 +(TLRef i))) H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) +H3)) H2))) | (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) +(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T +(TLRef i2) (THead (Bind b) v t))).((let H3 \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 (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in (False_ind ((eq T +(TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | (iso_head k v1 v2 t2 t3) +\Rightarrow (\lambda (H1: (eq T (THead k v1 t2) (THead (Flat f) t0 (THeads +(Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T (THead k v2 t3) (THead (Bind b) +v t))).((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return +(\lambda (_: T).T) with [(TSort _) \Rightarrow t2 | (TLRef _) \Rightarrow t2 +| (THead _ _ t) \Rightarrow t])) (THead k v1 t2) (THead (Flat f) t0 (THeads +(Flat f) t1 (TLRef i))) H1) in ((let H4 \def (f_equal T T (\lambda (e: +T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | +(TLRef _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t2) +(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in ((let H5 \def +(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with +[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) +\Rightarrow k])) (THead k v1 t2) (THead (Flat f) t0 (THeads (Flat f) t1 +(TLRef i))) H1) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T v1 t0) \to ((eq +T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead k0 v2 t3) (THead (Bind +b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 (\lambda (_: +T).((eq T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead (Flat f) v2 +t3) (THead (Bind b) v t)) \to P))) (\lambda (H7: (eq T t2 (THeads (Flat f) t1 +(TLRef i)))).(eq_ind T (THeads (Flat f) t1 (TLRef i)) (\lambda (_: T).((eq T +(THead (Flat f) v2 t3) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T +(THead (Flat f) v2 t3) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead +(Flat f) v2 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) +with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ +_) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) +\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) +in (False_ind P H9))) t2 (sym_eq T t2 (THeads (Flat f) t1 (TLRef i)) H7))) v1 +(sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f) H5))) H4)) H3)) H2)))]) in (H1 +(refl_equal T (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) (refl_equal +T (THead (Bind b) v t))))))))) vs)))))). + +theorem iso_flats_flat_bind_false: + \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall +(v2: T).(\forall (t: T).(\forall (t2: T).(\forall (vs: TList).((iso (THeads +(Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to (\forall (P: +Prop).P))))))))) +\def + \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda +(v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind +(\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2)) +(THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead +(Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 \def +(match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: (iso t0 +t1)).((eq T t0 (THead (Flat f2) v2 t2)) \to ((eq T t1 (THead (Bind b) v t)) +\to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1) +(THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v +t))).((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 (Flat f2) v2 +t2) H0) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H2)) +H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (THead +(Flat f2) v2 t2))).(\lambda (H1: (eq T (TLRef i2) (THead (Bind b) v +t))).((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 (Flat f2) v2 +t2) H0) in (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H2)) +H1))) | (iso_head k v1 v0 t1 t0) \Rightarrow (\lambda (H0: (eq T (THead k v1 +t1) (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (THead k v0 t0) (THead +(Bind b) v t))).((let H2 \def (f_equal T T (\lambda (e: T).(match e in T +return (\lambda (_: T).T) with [(TSort _) \Rightarrow t1 | (TLRef _) +\Rightarrow t1 | (THead _ _ t) \Rightarrow t])) (THead k v1 t1) (THead (Flat +f2) v2 t2) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T +return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) +\Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t1) (THead (Flat +f2) v2 t2) H0) in ((let H4 \def (f_equal T K (\lambda (e: T).(match e in T +return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) +\Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v1 t1) (THead (Flat +f2) v2 t2) H0) in (eq_ind K (Flat f2) (\lambda (k0: K).((eq T v1 v2) \to ((eq +T t1 t2) \to ((eq T (THead k0 v0 t0) (THead (Bind b) v t)) \to P)))) (\lambda +(H5: (eq T v1 v2)).(eq_ind T v2 (\lambda (_: T).((eq T t1 t2) \to ((eq T +(THead (Flat f2) v0 t0) (THead (Bind b) v t)) \to P))) (\lambda (H6: (eq T t1 +t2)).(eq_ind T t2 (\lambda (_: T).((eq T (THead (Flat f2) v0 t0) (THead (Bind +b) v t)) \to P)) (\lambda (H7: (eq T (THead (Flat f2) v0 t0) (THead (Bind b) +v t))).(let H8 \def (eq_ind T (THead (Flat f2) v0 t0) (\lambda (e: T).(match +e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | +(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return +(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow +True])])) I (THead (Bind b) v t) H7) in (False_ind P H8))) t1 (sym_eq T t1 t2 +H6))) v1 (sym_eq T v1 v2 H5))) k (sym_eq K k (Flat f2) H4))) H3)) H2)) +H1)))]) in (H0 (refl_equal T (THead (Flat f2) v2 t2)) (refl_equal T (THead +(Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: (((iso +(THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to +(\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads (Flat +f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P: +Prop).(let H1 \def (match H0 in iso return (\lambda (t3: T).(\lambda (t4: +T).(\lambda (_: (iso t3 t4)).((eq T t3 (THead (Flat f1) t0 (THeads (Flat f1) +t1 (THead (Flat f2) v2 t2)))) \to ((eq T t4 (THead (Bind b) v t)) \to P))))) +with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) (THead +(Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: +(eq T (TSort n2) (THead (Bind b) v t))).((let H3 \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 (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) +H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H3)) H2))) | +(iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) (THead (Flat f1) +t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: (eq T +(TLRef i2) (THead (Bind b) v t))).((let H3 \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 (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in +(False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | +(iso_head k v1 v0 t3 t4) \Rightarrow (\lambda (H1: (eq T (THead k v1 t3) +(THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda +(H2: (eq T (THead k v0 t4) (THead (Bind b) v t))).((let H3 \def (f_equal T T +(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) +\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t) \Rightarrow t])) +(THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 +t2))) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return +(\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 +| (THead _ t _) \Rightarrow t])) (THead k v1 t3) (THead (Flat f1) t0 (THeads +(Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in ((let H5 \def (f_equal T K +(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) +\Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) +(THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 +t2))) H1) in (eq_ind K (Flat f1) (\lambda (k0: K).((eq T v1 t0) \to ((eq T t3 +(THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to ((eq T (THead k0 v0 t4) +(THead (Bind b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 +(\lambda (_: T).((eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to +((eq T (THead (Flat f1) v0 t4) (THead (Bind b) v t)) \to P))) (\lambda (H7: +(eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))).(eq_ind T (THeads +(Flat f1) t1 (THead (Flat f2) v2 t2)) (\lambda (_: T).((eq T (THead (Flat f1) +v0 t4) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T (THead (Flat f1) v0 +t4) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead (Flat f1) v0 t4) +(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) +\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow +(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | +(Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) in (False_ind P +H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1 +(sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f1) H5))) H4)) H3)) H2)))]) in (H1 +(refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 +t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma new file mode 100644 index 000000000..4823ffdbf --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||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/iso/props". + +include "iso/defs.ma". + +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))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs.ma new file mode 100644 index 000000000..c98208a78 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/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/r/defs". + +include "T/defs.ma". + +definition r: + K \to (nat \to nat) +\def + \lambda (k: K).(\lambda (i: nat).(match k with [(Bind _) \Rightarrow i | +(Flat _) \Rightarrow (S i)])). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma new file mode 100644 index 000000000..709e13bb8 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/r/props". + +include "r/defs.ma". + +include "s/defs.ma". + +theorem r_S: + \forall (k: K).(\forall (i: nat).(eq nat (r k (S i)) (S (r k i)))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (r k0 (S +i)) (S (r k0 i))))) (\lambda (b: B).(\lambda (i: nat).(refl_equal nat (S (r +(Bind b) i))))) (\lambda (f: F).(\lambda (i: nat).(refl_equal nat (S (r (Flat +f) i))))) k). + +theorem r_plus: + \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) +(plus (r k i) j)))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: +nat).(eq nat (r k0 (plus i j)) (plus (r k0 i) j))))) (\lambda (b: B).(\lambda +(i: nat).(\lambda (j: nat).(refl_equal nat (plus (r (Bind b) i) j))))) +(\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (r +(Flat f) i) j))))) k). + +theorem r_plus_sym: + \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) +(plus i (r k j))))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: +nat).(eq nat (r k0 (plus i j)) (plus i (r k0 j)))))) (\lambda (_: B).(\lambda +(i: nat).(\lambda (j: nat).(refl_equal nat (plus i j))))) (\lambda (_: +F).(\lambda (i: nat).(\lambda (j: nat).(plus_n_Sm i j)))) k). + +theorem r_minus: + \forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (k: K).(eq nat +(minus (r k i) (S n)) (r k (minus i (S n))))))) +\def + \lambda (i: nat).(\lambda (n: nat).(\lambda (H: (lt n i)).(\lambda (k: +K).(K_ind (\lambda (k0: K).(eq nat (minus (r k0 i) (S n)) (r k0 (minus i (S +n))))) (\lambda (_: B).(refl_equal nat (minus i (S n)))) (\lambda (_: +F).(minus_x_Sy i n H)) k)))). + +theorem r_dis: + \forall (k: K).(\forall (P: Prop).(((((\forall (i: nat).(eq nat (r k i) i))) +\to P)) \to (((((\forall (i: nat).(eq nat (r k i) (S i)))) \to P)) \to P))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (P: Prop).(((((\forall (i: +nat).(eq nat (r k0 i) i))) \to P)) \to (((((\forall (i: nat).(eq nat (r k0 i) +(S i)))) \to P)) \to P)))) (\lambda (b: B).(\lambda (P: Prop).(\lambda (H: +((((\forall (i: nat).(eq nat (r (Bind b) i) i))) \to P))).(\lambda (_: +((((\forall (i: nat).(eq nat (r (Bind b) i) (S i)))) \to P))).(H (\lambda (i: +nat).(refl_equal nat i))))))) (\lambda (f: F).(\lambda (P: Prop).(\lambda (_: +((((\forall (i: nat).(eq nat (r (Flat f) i) i))) \to P))).(\lambda (H0: +((((\forall (i: nat).(eq nat (r (Flat f) i) (S i)))) \to P))).(H0 (\lambda +(i: nat).(refl_equal nat (S i)))))))) k). + +theorem s_r: + \forall (k: K).(\forall (i: nat).(eq nat (s k (r k i)) (S i))) +\def + \lambda (k: K).(match k in K return (\lambda (k0: K).(\forall (i: nat).(eq +nat (s k0 (r k0 i)) (S i)))) with [(Bind _) \Rightarrow (\lambda (i: +nat).(refl_equal nat (S i))) | (Flat _) \Rightarrow (\lambda (i: +nat).(refl_equal nat (S i)))]). + +theorem r_arith0: + \forall (k: K).(\forall (i: nat).(eq nat (minus (r k (S i)) (S O)) (r k i))) +\def + \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (S (r k i)) (\lambda (n: +nat).(eq nat (minus n (S O)) (r k i))) (eq_ind_r nat (r k i) (\lambda (n: +nat).(eq nat n (r k i))) (refl_equal nat (r k i)) (minus (S (r k i)) (S O)) +(minus_Sx_SO (r k i))) (r k (S i)) (r_S k i))). + +theorem r_arith1: + \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (r k (S +i)) (S j)) (minus (r k i) j)))) +\def + \lambda (k: K).(\lambda (i: nat).(\lambda (j: nat).(eq_ind_r nat (S (r k i)) +(\lambda (n: nat).(eq nat (minus n (S j)) (minus (r k i) j))) (refl_equal nat +(minus (r k i) j)) (r k (S i)) (r_S k i)))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma new file mode 100644 index 000000000..7245a89ff --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tlt/defs". + +include "T/defs.ma". + +definition wadd: + ((nat \to nat)) \to (nat \to (nat \to nat)) +\def + \lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n +with [O \Rightarrow w | (S m) \Rightarrow (f m)]))). + +definition weight_map: + ((nat \to nat)) \to (T \to nat) +\def + let rec weight_map (f: ((nat \to nat))) (t: T) on t: nat \def (match t with +[(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0) +\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr +\Rightarrow (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f +u))) t0))) | Abst \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f +O) t0))) | Void \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f O) +t0)))]) | (Flat _) \Rightarrow (S (plus (weight_map f u) (weight_map f +t0)))])]) in weight_map. + +definition weight: + T \to nat +\def + weight_map (\lambda (_: nat).O). + +definition tlt: + T \to (T \to Prop) +\def + \lambda (t1: T).(\lambda (t2: T).(lt (weight t1) (weight t2))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma new file mode 100644 index 000000000..caeac0dbd --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma @@ -0,0 +1,302 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tlt/props". + +include "tlt/defs.ma". + +theorem wadd_le: + \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: +nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to +(\forall (n: nat).(le (wadd f v n) (wadd g w n)))))))) +\def + \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: +((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w: +nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: +nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le +(wadd f v n0) (wadd g w n0))).(H n0))) n))))))). + +theorem wadd_lt: + \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: +nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to +(\forall (n: nat).(le (wadd f v n) (wadd g w n)))))))) +\def + \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: +((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w: +nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: +nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0)) +(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0))) +n))))))). + +theorem wadd_O: + \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O) +\def + \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_: +nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat +(wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n). + +theorem weight_le: + \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t) +(weight_map g t))))) +\def + \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to +nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) +\to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda +(f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (n: +nat).(le (f n) (g n))))).(le_n (weight_map g (TSort n))))))) (\lambda (n: +nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: +((\forall (n: nat).(le (f n) (g n))))).(H n))))) (\lambda (k: K).(K_ind +(\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall +(g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le +(weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: +((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) +(g n)))) \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: +((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) +(g n)))) \to (le (weight_map f (THead k0 t0 t1)) (weight_map g (THead k0 t0 +t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (t0: +T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall +(n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g t0)))))) +\to (\forall (t1: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) +(weight_map g t1)))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat +\to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (match b0 with +[Abbr \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f (S +(weight_map f t0))) t1))) | Abst \Rightarrow (S (plus (weight_map f t0) +(weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus (weight_map f t0) +(weight_map (wadd f O) t1)))]) (match b0 with [Abbr \Rightarrow (S (plus +(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))) | Abst +\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) | Void +\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O) +t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to +nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) +\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda +(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall +(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g +t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to +nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus +(weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus +(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1)) +(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S +(weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g +H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0))) +(\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0)) +(le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n)))))))))))) +(\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: +((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f +t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: +((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) +(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat +\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le +(f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O) +t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S +(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g +t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map +(wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1)) +(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O) +t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda +(n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) (\lambda (t0: +T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) +(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat +\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g +n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat +\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le +(f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O) +t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S +(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g +t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map +(wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1)) +(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O) +t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda +(n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) b)) (\lambda (_: +F).(\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: +((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f +t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: +((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) +(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f0: +((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: +nat).(le (f0 n) (g n))))).(lt_le_S (plus (weight_map f0 t0) (weight_map f0 +t1)) (S (plus (weight_map g t0) (weight_map g t1))) (le_lt_n_Sm (plus +(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g +t1)) (plus_le_compat (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1) +(weight_map g t1) (H f0 g H1) (H0 f0 g H1)))))))))))) k)) t). + +theorem weight_eq: + \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f +t) (weight_map g t))))) +\def + \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to +nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym +(weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n: +nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n) +(H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0: +nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))). + +theorem weight_add_O: + \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t) +(weight_map (\lambda (_: nat).O) t)) +\def + \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_: +nat).O) (\lambda (n: nat).(wadd_O n))). + +theorem weight_add_S: + \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O) +O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t))) +\def + \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O) +(wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(le_S_n (wadd (\lambda +(_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (le_n_S (wadd (\lambda +(_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (wadd_le (\lambda (_: +nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_O_n (S +m)) n)))))). + +theorem tlt_trans: + \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to +(tlt u t))))) +\def + \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u) +(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u) +(weight v) (weight t) H H0))))). + +theorem tlt_head_sx: + \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t)))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt +(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead +k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall +(t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr +\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd +(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst +\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd +(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda +(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda +(u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S +(plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: +nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (le_n_S (S (weight_map +(\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) +(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) +u))) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map +(\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map +(\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u) +(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) +u))) t))))))) (\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda +(_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map +(wadd (\lambda (_: nat).O) O) t))) (le_n_S (S (weight_map (\lambda (_: +nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd +(\lambda (_: nat).O) O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) +(plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: +nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map +(wadd (\lambda (_: nat).O) O) t))))))) (\lambda (u: T).(\lambda (t: +T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map +(\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))) +(le_n_S (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda +(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))) (le_n_S +(weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) +(weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda +(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))))))) b)) +(\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map +(\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) +(weight_map (\lambda (_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_: +nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda +(_: nat).O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus +(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)) +(le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: +nat).O) t)))))))) k). + +theorem tlt_head_dx: + \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t)))) +\def + \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt +(weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead +k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall +(t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr +\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd +(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst +\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd +(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda +(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda +(u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S +(weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_: +nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: +nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S +(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) +(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) +u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd +(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus +(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S +(weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd +(\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda +(_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t +(weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t) +(weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map +(wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))))))) +(\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_: +nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus +(weight_map (\lambda (_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_: +nat).O) t)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda +(_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus +(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) +(le_n_S (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: +nat).O) u) (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map +(\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))))) (weight_map +(wadd (\lambda (_: nat).O) O) t) (weight_add_O t)))) (\lambda (u: T).(\lambda +(t: T).(eq_ind_r nat (weight_map (\lambda (_: nat).O) t) (\lambda (n: +nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus (weight_map (\lambda +(_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus +(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) +(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda +(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map +(\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map +(\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) +(weight_map (\lambda (_: nat).O) t))))) (weight_map (wadd (\lambda (_: +nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u: +T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus +(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) +(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda +(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map +(\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map +(\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) +(weight_map (\lambda (_: nat).O) t)))))))) k). + +theorem tlt_wf__q_ind: + \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P: ((T \to +Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P +t))))) P n))) \to (\forall (t: T).(P t))) +\def + let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: +T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to +Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t) +n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight +t)))))). + +theorem tlt_wf_ind: + \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t) +\to (P v)))) \to (P t)))) \to (\forall (t: T).(P t))) +\def + let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: +T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to +Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v) +(weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind +(\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0: +T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) +\to (Q (\lambda (t: T).(P t)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat +(weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: nat).(\forall (m: +nat).((lt m n) \to (\forall (t: T).((eq nat (weight t) m) \to (P t)))))) H0 +(weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt (weight v) (weight +t0))).(H2 (weight v) H3 v (refl_equal nat (weight v))))))))))))) t)))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma index f0db3d133..de2399b05 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma @@ -17,10 +17,16 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems". -include "LambdaDelta-6.ma". +include "LambdaDelta/theory.ma". (* +(* Problem 2: disambiguation errors with these objects *) + +iso_trans (in iso/props) + +drop1_getl_trans + (* Problem 1: does not typecheck a match on an empty type *) theorem subst0_confluence_neq: @@ -28,10 +34,6 @@ theorem subst0_confluence_neq: \def \lambda (t0: T).(\lambda (t1: T).(\lambda (u1: T).(\lambda (i1: nat).(\lambda (H: (subst0 i1 u1 t0 t1)).(subst0_ind (\lambda (n: nat).(\lambda (t: T).(\lambda (t2: T).(\lambda (t3: T).(\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq nat n i2)) \to (ex2 T (\lambda (t5: T).(subst0 i2 u2 t3 t5)) (\lambda (t5: T).(subst0 n t t4 t5)))))))))))) (\lambda (v: T).(\lambda (i: nat).(\lambda (t2: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H0: (subst0 i2 u2 (TLRef i) t2)).(\lambda (H1: (not (eq nat i i2))).(and_ind (eq nat i i2) (eq T t2 (lift (S i) O u2)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v) t)) (\lambda (t: T).(subst0 i v t2 t))) (\lambda (H2: (eq nat i i2)).(\lambda (H3: (eq T t2 (lift (S i) O u2))).(let H4 \def (eq_ind nat i (\lambda (n: nat).(not (eq nat n i2))) H1 i2 H2) in (eq_ind_r T (lift (S i) O u2) (\lambda (t: T).(ex2 T (\lambda (t3: T).(subst0 i2 u2 (lift (S i) O v) t3)) (\lambda (t3: T).(subst0 i v t t3)))) (let H5 \def (match (H4 (refl_equal nat i2)) return (\lambda (_: False).(ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v) t)) (\lambda (t: T).(subst0 i v (lift (S i) O u2) t)))) with []) in H5) t2 H3)))) (subst0_gen_lref u2 t2 i2 i H0))))))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u0: T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: ((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (t: T).(\lambda (k: K).(\lambda (t2: T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u3 (THead k u0 t) t2)).(\lambda (H3: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex3_2 T T (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3)))) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (H4: (ex2 T (\lambda (u2: T).(eq T t2 (THead k u2 t))) (\lambda (u2: T).(subst0 i2 u3 u0 u2)))).(ex2_ind T (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4: T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq T t2 (THead k x t))).(\lambda (H6: (subst0 i2 u3 u0 x)).(eq_ind_r T (THead k x t) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i v x t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x t) t3))) (\lambda (x0: T).(\lambda (H7: (subst0 i2 u3 u2 x0)).(\lambda (H8: (subst0 i v x x0)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x t) t3)) (THead k x0 t) (subst0_fst u3 x0 u2 i2 H7 t k) (subst0_fst v x0 x i H8 t k))))) (H1 x u3 i2 H6 H3)) t2 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t2: T).(subst0 (s k i2) u3 t t2)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq T t2 (THead k u0 x))).(\lambda (H6: (subst0 (s k i2) u3 t x)).(eq_ind_r T (THead k u0 x) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k u0 x) t3)) (THead k u2 x) (subst0_snd k u3 x t i2 H6 u2) (subst0_fst v u2 u0 i H0 x k)) t2 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i2) u3 t t2))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t2 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u3 u0 x0)).(\lambda (H7: (subst0 (s k i2) u3 t x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i v x0 t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x0 x1) t3))) (\lambda (x: T).(\lambda (H8: (subst0 i2 u3 u2 x)).(\lambda (H9: (subst0 i v x0 x)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x0 x1) t3)) (THead k x x1) (subst0_both u3 u2 x i2 H8 k t x1 H7) (subst0_fst v x x0 i H9 x1 k))))) (H1 x0 u3 i2 H6 H3)) t2 H5)))))) H4)) (subst0_gen_head k u3 u0 t t2 i2 H2))))))))))))))) (\lambda (k: K).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H0: (subst0 (s k i) v t3 t2)).(\lambda (H1: ((\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t3 t4) \to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u2 (THead k u t3) t4)).(\lambda (H3: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3))) (ex2 T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))) (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5)))) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (H4: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3)))).(ex2_ind T (\lambda (u3: T).(eq T t4 (THead k u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H5: (eq T t4 (THead k x t3))).(\lambda (H6: (subst0 i2 u2 u x)).(eq_ind_r T (THead k x t3) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x t3) t)) (THead k x t2) (subst0_fst u2 x u i2 H6 t2 k) (subst0_snd k v t2 t3 i H0 x)) t4 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u t2))) (\lambda (t2: T).(subst0 (s k i2) u2 t3 t2)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2) u2 t3 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H5: (eq T t4 (THead k u x))).(\lambda (H6: (subst0 (s k i2) u2 t3 x)).(eq_ind_r T (THead k u x) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k u x) t))) (\lambda (x0: T).(\lambda (H7: (subst0 (s k i2) u2 t2 x0)).(\lambda (H8: (subst0 (s k i) v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k u x) t)) (THead k u x0) (subst0_snd k u2 x0 t2 i2 H7 u) (subst0_snd k v x0 x i H8 u))))) (H1 x u2 (s k i2) H6 (\lambda (H7: (eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H7))))) t4 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i2) u2 t3 t2))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t4 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u2 u x0)).(\lambda (H7: (subst0 (s k i2) u2 t3 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i2) u2 t2 x)).(\lambda (H9: (subst0 (s k i) v x1 x)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k x0 x) (subst0_both u2 u x0 i2 H6 k t2 x H8) (subst0_snd k v x x1 i H9 x0))))) (H1 x1 u2 (s k i2) H7 (\lambda (H8: (eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H8))))) t4 H5)))))) H4)) (subst0_gen_head k u2 u t3 t4 i2 H2))))))))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: ((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (k: K).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2: (subst0 (s k i) v t2 t3)).(\lambda (H3: ((\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t3 t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (t4: T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H4: (subst0 i2 u3 (THead k u0 t2) t4)).(\lambda (H5: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex3_2 T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5)))) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2 t2))) (\lambda (u2: T).(subst0 i2 u3 u0 u2)))).(ex2_ind T (\lambda (u4: T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H7: (eq T t4 (THead k x t2))).(\lambda (H8: (subst0 i2 u3 u0 x)).(eq_ind_r T (THead k x t2) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x t2) t))) (\lambda (x0: T).(\lambda (H9: (subst0 i2 u3 u2 x0)).(\lambda (H10: (subst0 i v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x t2) t)) (THead k x0 t3) (subst0_fst u3 x0 u2 i2 H9 t3 k) (subst0_both v x x0 i H10 k t2 t3 H2))))) (H1 x u3 i2 H8 H5)) t4 H7)))) H6)) (\lambda (H6: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u0 t2))) (\lambda (t3: T).(subst0 (s k i2) u3 t2 t3)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2) u3 t2 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H7: (eq T t4 (THead k u0 x))).(\lambda (H8: (subst0 (s k i2) u3 t2 x)).(eq_ind_r T (THead k u0 x) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k u0 x) t))) (\lambda (x0: T).(\lambda (H9: (subst0 (s k i2) u3 t3 x0)).(\lambda (H10: (subst0 (s k i) v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k u0 x) t)) (THead k u2 x0) (subst0_snd k u3 x0 t3 i2 H9 u2) (subst0_both v u0 u2 i H0 k x x0 H10))))) (H3 x u3 (s k i2) H8 (\lambda (H9: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H9))))) t4 H7)))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t2 t3))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T t4 (THead k x0 x1))).(\lambda (H8: (subst0 i2 u3 u0 x0)).(\lambda (H9: (subst0 (s k i2) u3 t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v x0 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H10: (subst0 i2 u3 u2 x)).(\lambda (H11: (subst0 i v x0 x)).(ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x2: T).(\lambda (H12: (subst0 (s k i2) u3 t3 x2)).(\lambda (H13: (subst0 (s k i) v x1 x2)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k x x2) (subst0_both u3 u2 x i2 H10 k t3 x2 H12) (subst0_both v x0 x i H11 k x1 x2 H13))))) (H3 x1 u3 (s k i2) H9 (\lambda (H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))) (H1 x0 u3 i2 H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2 H4)))))))))))))))))) i1 u1 t0 t1 H))))). -(* Problem 2: disambiguation errors with these objects *) - -iso_trans drop1_getl_trans - (* Problem 3: assertion failure raised by type checker on this object *) tau1 -- 2.39.2