From 4d18494d87350c31e679a540bb2638cd821343f4 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 18:01:33 +0000 Subject: [PATCH] commit by user ricciott --- weblib/cr/lambda.ma | 1696 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1696 insertions(+) create mode 100644 weblib/cr/lambda.ma diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma new file mode 100644 index 000000000..493f63304 --- /dev/null +++ b/weblib/cr/lambda.ma @@ -0,0 +1,1696 @@ +include "basics/list.ma". +include "basics/types.ma". + +(* LIST THEORY *) +(*theorem nil_cons: + ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. +#A;#l;#a; @; #H; ndestruct; +nqed. + +ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l. +#A;#l;nelim l;//; +#a;#l1;#IH;nnormalize;//; +nqed. + +ntheorem associative_append: ∀A:Type[0].associative (list A) (append A). +#A;#x;#y;#z;nelim x +##[// +##|#a;#x1;#H;nnormalize;//] +nqed. + +ntheorem cons_append_commute: + ∀A:Type[0].∀l1,l2:list A.∀a:A. + a :: (l1 @ l2) = (a :: l1) @ l2. +//; +nqed. + +nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1. +#A;#a;#l;#l1;nrewrite > (associative_append ????);//; +nqed. + + +nlet rec nth A l d n on n ≝ + match n with + [ O ⇒ match l with + [ nil ⇒ d + | cons (x : A) _ ⇒ x ] + | S n' ⇒ nth A (tail ? l) d n']. + +nlet rec map A B f l on l ≝ + match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. + +nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ + match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ]. + +ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l. + +ndefinition filter ≝ + λT:Type[0].λl:list T.λp:T → bool. + foldr T (list T) + (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l. + +ndefinition iota : nat → nat → list nat ≝ + λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. +*) +(* ### induction principle for functions visiting 2 lists in parallel *) +lemma list_ind2 : + ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1 → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2 → Prop. + a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l2 → + (P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?)) → + (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1a title="cons" href="cic:/fakeuri.def(1)":/a:tl1) (hd2a title="cons" href="cic:/fakeuri.def(1)":/a:tl2)) → + P l1 l2. +#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons +generalize in match Hl; generalize in match l2; +elim l1 +[#l2 cases l2 // + normalize #t2 #tl2 #H destruct +|#t1 #tl1 #IH #l2 cases l2 + [normalize #H destruct + |#t2 #tl2 #H @Pcons @IH normalize in H;destruct //] +] +qed. + +lemma eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l. +#A #B #f #g #l #Efg +elim l normalize // +qed. + +lemma le_length_filter : ∀A,l,p.a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A l. +#A #l #p elim l normalize +[// +|#a #tl #IH cases (p a) normalize + [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // + |%2 // + ] +] +qed. + +lemma length_append : ∀A,l,m.a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A (la title="append" href="cic:/fakeuri.def(1)"@/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A l a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A m. +#A #l #m elim l +[// +|#H #tl #IH normalize (H ? ? H3);apply in_list_head + |intro;rewrite > H3 in H2;simplify in H2; + apply in_list_cons;apply H1;assumption]] +qed.*) + +naxiom in_list_to_mem_true : + \forall A,equ. + (\forall x.equ x x = true) \to + \forall x,l.in_list A x l \to mem A equ x l = true. +(*intros 5.elim l + [elim (not_in_list_nil ? ? H1) + |elim H2 + [simplify;rewrite > H;reflexivity + |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. +qed.*) + +naxiom in_list_filter_to_p_true : \forall A,l,x,p. +in_list A x (filter A l p) \to p x = true. +(* intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;assumption + |apply (H H3)] + |apply (H H1)]] +qed.*) + +naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. +(*intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;apply in_list_head + |apply in_list_cons;apply H;assumption] + |apply in_list_cons;apply H;assumption]] +qed.*) + +naxiom in_list_filter_r : \forall A,l,p,x. + in_list A x l \to p x = true \to in_list A x (filter A l p). +(* intros 4;elim l + [elim (not_in_list_nil ? ? H) + |elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head + |simplify;apply (bool_elim ? (p a));intro;simplify; + [apply in_list_cons;apply H;assumption + |apply H;assumption]]] +qed.*) + +naxiom incl_A_A: ∀T,A.incl T A A. +(*intros.unfold incl.intros.assumption. +qed.*) + +naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. +qed.*) + +*) + + +record Nset : Type[1] ≝ +{ + (* carrier is specified as a coercion: when an object X of type Nset is + given, but something of type Type is expected, Matita will insert a + hidden coercion: the user sees "X", but really means "carrier X" *) + carrier :> Type[0]; + N_eqb : carrier → carrier → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a; + p_eqb1 : ∀x,y.N_eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y; + p_eqb2 : ∀x,y.N_eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y; + N_fresh : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a carrier → carrier; + p_fresh : ∀l.N_fresh l a title="list not member" href="cic:/fakeuri.def(1)"∉/a l +}. + +lemma bool_elim : +∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.∀b.(b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P b. +#P * /span class="autotactic"2span class="autotrace" trace /span/span/ +qed. + +lemma p_eqb3 : ∀X,x,y.x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#X #x #y @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y)) // +#H1 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H1) #H2 #H3 cases (H2 H3) +qed. + +lemma p_eqb4 : ∀X,x,y.x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#X #x #y #H1 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y)) // +#H2 cases H1 #H3 cases (H3 (a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a ??? H2)) +qed. + +axiom X : a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a. + +inductive pre_tm : Type[0] ≝ +| Par : a href="cic:/matita/cr/lambda/X.dec"X/a → pre_tm +| Var : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → pre_tm +| App : pre_tm → pre_tm → pre_tm +| Abs : pre_tm → pre_tm. + +inductive tm_level : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ +| tml_Par : ∀n,x.tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) +| tml_Var : ∀n,m.n a title="natural 'greater than'" href="cic:/fakeuri.def(1)">/a m → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a m) +| tml_App : ∀n,M1,M2.tm_level n M1 → tm_level n M2 → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2) +| tml_Abs : ∀n,M0.tm_level (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) M0 → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M0). + +record ext_tm (l:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : Type[0] ≝ { + tm_of_etm :> a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a; + etm_level : a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"tm_level/a l tm_of_etm +}. + +(* + * we don't want to specify "N_eqb X" or "N_eqb Y" for the equality on X or Y, + * so we use a notation "a ? b" to hide the naming structure + * to type ?, write \equest. + *) +notation > "hvbox(a break ≟ b)" + non associative with precedence 40 +for @{ 'equiv ? $a $b }. +notation < "hvbox(a break maction (≟) (≟\sub t) b)" + non associative with precedence 40 +for @{ 'equiv $t $a $b }. +interpretation "name decidable equality" 'equiv t a b = (N_eqb t a b). + +(* valida solo se u è chiuso *) +let rec subst t x u on t : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a ≝ + match t with + [ Par x2 ⇒ match x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x2 with + [ true ⇒ u + | false ⇒ t ] + | Var _ ⇒ t + | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (subst t1 x u) (subst t2 x u) + | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (subst t1 x u) ]. + +let rec nth A (xl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) n on xl ≝ + match xl with + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a A + | cons x0 xl0 ⇒ match n with + [ O ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a A x0 + | S m ⇒ nth A xl0 m ] ]. + +(* it's necessary to specify Nset... unification hint? *) +let rec posn (A:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a) (xl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) x on xl ≝ + match xl with + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a + | cons x0 xl0 ⇒ match x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0 with + [ true ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | false ⇒ match posn A xl0 x with + [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a + | Some n ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) ] ] ]. + +let rec vopen t xl k on t ≝ + match t with + [ Par _ ⇒ t + | Var n ⇒ match a href="cic:/matita/cr/lambda/nth.fix(0,1,1)"nth/a ? xl (na title="natural plus" href="cic:/fakeuri.def(1)"+/ak) with + [ None ⇒ t + | Some x ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x ] + | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (vopen t1 xl k) (vopen t2 xl k) + | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (vopen t1 xl (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k)) ]. + +let rec vclose t xl k on t ≝ + match t with + [ Par x0 ⇒ match a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? xl x0 with + [ None ⇒ t + | Some n ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ak) ] + | Var n ⇒ t + | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (vclose t1 xl k) (vclose t2 xl k) + | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (vclose t1 xl (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k)) ]. + +let rec GV t ≝ + match t with + [ Par x ⇒ xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] + | Var _ ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] + | App u v ⇒ GV u a title="append" href="cic:/fakeuri.def(1)"@/a GV v + | Abs u ⇒ GV u ]. + +(* as above, fp_perm is a coercion + * but being a coercion to FunClass, a different syntax is required + * I'll fix this later *) +record fp (X:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a) : Type[0] ≝ +{ + fp_perm :1> X → X; + fp_injective : a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? fp_perm; + fp_surjective : a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? fp_perm; + fp_finite : a title="exists" href="cic:/fakeuri.def(1)"∃/al.∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → fp_perm x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x +}. + +definition Pi ≝ a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a. + +record fp_pre_tm : Type[0] ≝ +{ + fppt_perm :1> a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a; + fppt_injective : a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? fppt_perm; + fppt_surjective : a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? fppt_perm +}. + +(*coercion fp_perm : ∀N:Nset.∀F:fp N.N → N ≝ fp_perm on _F:(fp N) to ? → ?. +coercion fppt_perm : ∀F:fp_pre_tm.pre_tm → pre_tm ≝ fppt_perm on _F:fp_pre_tm to ? → ?.*) + +(* notation "p·x" right associative with precedence 60 for @{'middot $p $x}. +interpretation "apply fp" 'middot p x = (fp_perm ? p x). +interpretation "apply fppt" 'middot p x = (fppt_perm p x).*) + +let rec mapX (p:a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a) t on t : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a ≝ + match t with + [ Par x ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a (p x) + | Var _ ⇒ t + | App u v ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (mapX p u) (mapX p v) + | Abs u ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (mapX p u) ]. + +definition swap : ∀N:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a.N → N → N → N ≝ + λN,u,v,x.match (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u) with + [true ⇒ v + |false ⇒ match (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v) with + [true ⇒ u + |false ⇒ x]]. + +lemma Neqb_n_n : ∀N:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a.∀n:N.(n a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#N #n /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb3.def(4)"p_eqb3/a/span/span/ +qed. + +lemma swap_left : ∀N,x,y.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y. +#N #x #y whd in ⊢ (??%?); >(a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a) // +qed. + +lemma swap_right : ∀N,x,y.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y y) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#N #x #y whd in ⊢ (??%?); >(a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a) @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x)) +normalize #H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ +qed. + +lemma swap_other : ∀N,x,y,z.(z a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x) → (z a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y) → (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z. +#N #x #y #z #H1 #H2 normalize >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a … H1) +normalize >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a … H2) % +qed. + +lemma swap_inv : ∀N,u,v,x.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v x)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#N #u #v #x normalize +@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H1 >H1 normalize +[normalize >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize + @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (v a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H2 normalize + [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H1) % + |>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H1) % + ] +|@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) #H2 normalize + [>a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) % + |>H1 >H2 % + ] +] +qed. + +lemma swap_inj : ∀N,u,v.a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v). +#N #u #v #x #y normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H1 +[@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H2 + [#H3 >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3 + [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a ??? H3) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |#H4 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H3) #H5 cases (H5 ?) // + ] + ] +|@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H2 + [@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3 #H4 + [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3) + |>H4 in H3; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H5 destruct (H5) + ] + |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3 + [@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H4 #H5 + [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H4) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |>H5 in H2; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H2 destruct (H2) + ] + |cases (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v) normalize #H4 + [>H4 in H1; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H1 destruct (H1) + |// + ] + ] + ] +] +qed. + +lemma swap_surj : ∀N,u,v.a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v). +#N #u #v #z normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (z a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)); #H1 + [%[@u] >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (z a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H2 + [%[@v] + >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a ? v u) + [>a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |% #H3 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + ] + |%[@z] + >H1 >H2 % + ] + ] +qed. + +lemma swap_finite : ∀N,u,v.a title="exists" href="cic:/fakeuri.def(1)"∃/al.∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v) x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#N #u #v %[@ (ua title="cons" href="cic:/fakeuri.def(1)":/a:va title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a])] +#x #H1 @a href="cic:/matita/cr/lambda/swap_other.def(5)"swap_other/a % #H2 cases H1 #H3 @H3 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a, a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"in_list_cons/a/span/span/ +qed. + +definition pi_swap : ∀N,u,v.a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a N ≝ +λN,u,v.a href="cic:/matita/cr/lambda/fp.con(0,1,1)"mk_fp/a ? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v) (a href="cic:/matita/cr/lambda/swap_inj.def(6)"swap_inj/a N u v) (a href="cic:/matita/cr/lambda/swap_surj.def(6)"swap_surj/a N u v) (a href="cic:/matita/cr/lambda/swap_finite.def(6)"swap_finite/a N u v). + +lemma eq_swap_pi : ∀N,u,v,x.a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pi_swap.def(7)"pi_swap/a N u v x. +#N #u #v #x % +qed. + +(* lemma subst_fp : + ∀s,c,x.(x ∈ GV s → x = c) → subst_X s c (Par x) = (pi_swap ? c x)·s. +intros 3;elim s 0;simplify;intros +[rewrite < eq_swap_pi;apply (bool_elim ? (c ≟ c1));simplify;intro + [rewrite > (p_eqb1 ??? H1);autobatch + |apply (bool_elim ? (x ≟ c1));intro + [elim (p_eqb2 ??? H1);rewrite < H + [autobatch + |rewrite > (p_eqb1 ??? H2);autobatch] + |rewrite > swap_other;autobatch]] +|reflexivity +|rewrite > H + [rewrite > H1 + [reflexivity + |intro;apply H2;autobatch] + |intro;apply H2;autobatch] +|rewrite > H + [reflexivity + |assumption]] +qed. *) + +lemma subst_x_x : ∀M,x.a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M. +#M #x elim M normalize +[#x0 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ +|*:/span class="autotactic"2span class="autotrace" trace /span/span/] +qed. + +lemma pre_tm_inv_Par : + ∀P:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop. + ∀x.(∀x0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x0)) → ∀M.a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) M. +#P #x #H #M cases M +[// +|#n #H1 destruct (H1) +|#M1 #M2 #H1 destruct (H1) +|#M0 #H1 destruct (H1) +] +qed. + +lemma pre_tm_inv_Var : + ∀P:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop. + ∀n.(∀n0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n) (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0)) → ∀M.a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n) M. +#P #n #H #M cases M +[2:// +|#x #H1 destruct (H1) +|#M1 #M2 #H1 destruct (H1) +|#M0 #H1 destruct (H1) +] +qed. + +lemma pre_tm_inv_Lam : + ∀P:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop. + ∀M.(∀N0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M) (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0)) → ∀N.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a N → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M) N. +#P #M #H #N cases N +[4:// +|#x #H1 destruct (H1) +|#n #H1 destruct (H1) +|#M1 #M2 #H1 destruct (H1) +] +qed. + +lemma pre_tm_inv_App : + ∀P:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop. + ∀M1,M2.(∀N1,N2.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2) (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2)) → + ∀N.a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a N → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2) N. +#P #M1 #M2 #H #N cases N +[3:// +|#x #H1 destruct (H1) +|#n #H1 destruct (H1) +|#M0 #H1 destruct (H1) +] +qed. + +interpretation "permutation of pre_tm" 'middot p M = (mapX p M). + +lemma Pi_Par_elim : ∀P:Prop.∀p.∀x,y.(∀z.y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a z → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P. +#P #p #x #y cases y +[#x0 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/ +|#n #H1 #H2 normalize in H2; destruct (H2) +|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2) +|#M0 #H1 #H2 normalize in H2; destruct (H2) +] +qed. + +lemma Pi_Var_elim : ∀P:Prop.∀p,n,y.(∀n0.y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P. +#P #p #n #y cases y +[#x0 #H1 #H2 normalize in H2; destruct (H2) +|#n0 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/ +|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2) +|#M0 #H1 #H2 normalize in H2; destruct (H2) +] +qed. + +lemma Pi_App_elim : + ∀P:Prop.∀p,M1,M2,y.(∀N1,N2.y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P. +#P #p #M1 #M2 #y cases y +[#x0 #H1 #H2 normalize in H2; destruct (H2) +|#n #H1 #H2 normalize in H2; destruct (H2) +|#M1 #M2 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/ +|#M0 #H1 #H2 normalize in H2; destruct (H2) +] +qed. + +lemma Pi_Abs_elim : ∀P:Prop.∀p,M0,y.(∀N0.y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P. +#P #p #M0 #y cases y +[#x0 #H1 #H2 normalize in H2; destruct (H2) +|#n #H1 #H2 normalize in H2; destruct (H2) +|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2) +|#M0 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/ +] +qed. + +(*lemma mapX_elim : + ∀P:pre_tm → Prop.∀p,x,y.(∀z.P (p·z)) → p·x = y → P y. +#P #p #x #y #H1 *) + +definition fppt_of_fp : a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/fp_pre_tm.ind(1,0,0)"fp_pre_tm/a. +#p @a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"mk_fp_pre_tm/a +[@(a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"mapX/a p) +|#x elim x + [#x0 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"Pi_Par_elim/a … H1) + #z #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"fp_injective/a/span/span/ + |#n #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"Pi_Var_elim/a … H1) + #z #H2 >H2 in H1; #H1 @H1 + |#M1 #M2 #IH1 #IH2 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"Pi_App_elim/a … H1) + #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) + generalize in match e1; -e1 >e0 normalize in ⊢ (??%% → ?); #e1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a/span/span/ + |#M0 #IH0 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"Pi_Abs_elim/a … H1) + #N0 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a/span/span/ + ] +|#z elim z + [#x0 cases (a href="cic:/matita/cr/lambda/fp_surjective.fix(0,1,3)"fp_surjective/a ? p x0) #x1 #H1 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x1)] >H1 % + |#n0 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0)] % + |#M1 #M2 * #N1 #IH1 * #N2 #IH2 + %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2)] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a/span/span/ + |#M0 * #N0 #IH0 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0)] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a/span/span/ +] +qed. + +lemma pi_lemma1 : + ∀M,P,x,pi.pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x P) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a M) (pi x) (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a P). +#M #P #x #pi elim M +[#c normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a c)) normalize #H1 + [cut (pi x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pi c); + [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/ + |#H2 >a href="cic:/matita/cr/lambda/p_eqb3.def(4)"p_eqb3/a // ] + |cut (pi x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a pi c) + [% #H2 >(a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"fp_injective/a … H2) in H1; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H1 destruct (H1) + |#H2 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a // ] + ] +|*:normalize //] +qed. + +(* +lemma pi_lemma2 : + ∀M,P,y,pi. pi · (subst_Y M y P) = subst_Y (pi · M) y (pi · P). +intros;elim M +[reflexivity +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro;reflexivity +|simplify;autobatch paramodulation +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro;autobatch paramodulation] +qed. +*) + +definition Lam ≝ λx:a href="cic:/matita/cr/lambda/X.dec"X/a.λM:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a). + +definition Judg ≝ λG,M.a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M G a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. + +definition body ≝ λx,M.match M with + [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | _ ⇒ M ]. + +inductive L (F:X → S_exp → Y) : S_exp → Prop \def +| LPar : ∀x:X.L F (Par x) +| LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N) +| LAbs : ∀M:S_exp. ∀x:X. (L F M) → + L F (Abs (F x M) (subst_X M x (Var (F x M)))). + +definition apartb : X → S_exp → bool ≝ + λx,M.notb (mem X (N_eqb X) x (GV M)). + +let rec E (x:X) (M:S_exp) on M : list Y ≝ + match M with + [ Par x ⇒ [] + | Var _ ⇒ [] + | App u v ⇒ E x u @ E x v + | Abs y u ⇒ match apartb x u with + [ true ⇒ [] + | false ⇒ y :: E x u ]]. + +definition apart : X → S_exp → Prop ≝ + λx,M.¬ x ∈ GV M. + +interpretation "name apartness wrt GV" 'apart x s = (apart x s). + +lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s. +intros;intro; +lapply (in_list_to_mem_true ? (N_eqb X) ??? H1) +[simplify;intro;generalize in match (p_eqb2 ? x1 x1); + cases (x1 ≟ x1);intro;try autobatch; + elim H2;reflexivity; +|unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct] +qed. + +lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true. +intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true) +[unfold apartb;generalize in match Hcut; + cases (mem X (N_eqb X) x (GV s));intro; + [elim H1;reflexivity + |reflexivity] +|intro;apply H;autobatch] +qed. + +lemma E_fresh : ∀x,M.x # M → E x M = []. +intros 2;elim M;simplify +[1,2:reflexivity +|rewrite > H + [rewrite > H1 + [reflexivity + |elim s1 in H2;simplify; + [simplify in H2;intro;apply H2;autobatch + |autobatch + |simplify in H4;intro;apply H4;autobatch + |simplify in H3;intro;apply H3;autobatch]] + |elim s in H2;simplify; + [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3); + autobatch + |autobatch + |simplify in H4;intro;apply H4;autobatch + |simplify in H3;intro;apply H3;autobatch]] +|rewrite > H + [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity + |apply H1]] +qed. + +lemma mem_false_to_not_in_list : + ∀A,equ.(∀x,y.x = y → equ x y = true) → + ∀x,l.mem A equ x l = false → x ∉ l. +intros 5;elim l +[autobatch +|intro;apply (bool_elim ? (equ x a));intros + [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct + |cases (in_list_cons_case ???? H3) + [rewrite > H in H4 + [destruct + |assumption] + |apply H1; + [generalize in match H2;simplify;rewrite > H4;simplify; + intro;assumption + |assumption]]]] +qed. + +lemma mem_append : ∀A,equ. + (∀x,y. x = y → equ x y = true) → + (∀x,y. equ x y = true → x = y) → + ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2). +intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro +[cut (x ∈ l1@l2) + [cases (in_list_append_to_or_in_list ???? Hcut) + [rewrite > in_list_to_mem_true + [reflexivity + |intro;apply H;reflexivity + |assumption] + |cases (mem A equ x l1);simplify;try reflexivity; + rewrite > in_list_to_mem_true + [reflexivity + |intro;apply H;reflexivity + |assumption]] + |autobatch] +|lapply (mem_false_to_not_in_list ????? H2) + [assumption + |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify + [lapply (mem_true_to_in_list ????? H3);try assumption; + elim Hletin;autobatch + |apply (bool_elim ? (mem A equ x l2));intro;simplify + [lapply (mem_true_to_in_list ????? H4);try assumption; + elim Hletin;autobatch + |reflexivity]]]] +qed. + +(* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true. +simplify;intros;unfold apartb; +apply (bool_elim ? (mem X (N_eqb X) x (GV M))); +simplify;intro +[ + +cut (x ∉ GV M @ GV N) +[cut (apartb x M = false → False) + [generalize in match Hcut1;cases (apartb x M);simplify;intro; + [reflexivity|elim H1;reflexivity] + |intro;apply Hcut; + + +lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true. + +lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*) + +axiom daemon : False. + +lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q). +intros;elim M +[simplify;cases (x2 ≟ c);simplify;autobatch +|reflexivity +|simplify;autobatch +|whd in ⊢ (??%?);rewrite > H2; + simplify in ⊢ (???%); + rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q)) + [reflexivity + |elim s + [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro + [apply (bool_elim ? (x2 ≟ c1));simplify;intro + [lapply (p_eqb1 ??? H3);elim H;autobatch; + |rewrite > H3;reflexivity] + |apply (bool_elim ? (x2 ≟ c1));simplify;intro + [autobatch + |rewrite > H3;reflexivity]] + |reflexivity + |simplify;rewrite > mem_append + [rewrite > mem_append + [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation + |*:autobatch] + |*:autobatch] + |apply H3]]] +qed. + +lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M). +intros;reflexivity; +qed. + +lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M. +intros 4;simplify;cases (apartb x M);simplify;intro +[elim (not_in_list_nil ?? H) +|assumption] +qed. + +lemma E_all_fresh : ∀x1,x2,x3,M. + x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)). +intros;elim M;simplify +[cases (x1 ≟ c);reflexivity +|reflexivity +|autobatch paramodulation +|rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2))) + [rewrite > H2;reflexivity + |elim s + [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro + [lapply (p_eqb1 ??? H3);rewrite < Hletin; + rewrite > p_eqb4 [|assumption] + rewrite > p_eqb4 [|assumption] + reflexivity + |reflexivity] + |reflexivity + |simplify;rewrite > mem_append + [rewrite > mem_append + [unfold apartb in H3;unfold apartb in H4; + autobatch paramodulation + |*:autobatch] + |*:autobatch] + |apply H3]]] +qed. + +lemma E_fresh_subst_Y : + ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)). +intros;elim S +[reflexivity +|simplify;cases (y ≟ c);simplify;reflexivity +|simplify;autobatch paramodulation +|simplify;apply (bool_elim ? (y ≟ c));intro;simplify + [reflexivity + |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2))) + [reflexivity + |elim s;simplify + [reflexivity + |cases (y ≟ c1);simplify + [rewrite > p_eqb4;autobatch + |reflexivity] + |rewrite > mem_append [|*:autobatch] + rewrite > mem_append [|*:autobatch] + unfold apartb in H3;unfold apartb in H4; + autobatch paramodulation + |cases (y ≟ c1); simplify + [reflexivity + |apply H3]]]]] +qed. + +lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M. +intros 2; +elim M +[simplify;simplify in H; + rewrite > p_eqb4 + [reflexivity + |intro;apply H;autobatch] +|reflexivity +|simplify;rewrite > H + [rewrite > H1 + [reflexivity + |intro;apply H2;simplify;autobatch] + |intro;apply H2;simplify;autobatch] +|simplify;rewrite >H + [reflexivity + |apply H1]] +qed. + +lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M. +intros 2; +elim M +[reflexivity +|simplify;simplify in H; + rewrite > p_eqb4 + [reflexivity + |intro;apply H;autobatch] +|simplify;rewrite > H + [rewrite > H1 + [reflexivity + |intro;apply H2;simplify;autobatch] + |intro;apply H2;simplify;autobatch] +|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro + [reflexivity + |rewrite > H + [reflexivity + |intro;apply H1;apply in_list_filter_r;autobatch]]] +qed. + +lemma subst_X_lemma : + ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q → + subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q). +intros;elim M +[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro + [rewrite > p_eqb4 + [simplify;rewrite > H2;reflexivity + |intro;autobatch] + |apply (bool_elim ? (x2 ≟ c));simplify;intro + [rewrite > subst_X_apart;autobatch + |rewrite > H2;reflexivity]] +|reflexivity +|*:simplify;autobatch paramodulation] +qed. + +lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y). +intros 3;elim M +[simplify;simplify in H;rewrite > p_eqb4 + [reflexivity + |intro;autobatch] +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro + [rewrite > p_eqb3 [|reflexivity] + simplify;rewrite > (p_eqb1 ??? H1);reflexivity + |reflexivity] +|simplify;simplify in H2;rewrite < H; + [rewrite < H1 + [reflexivity + |intro;apply H2;autobatch] + |intro; apply H2;autobatch] +|simplify;simplify in H1;apply (bool_elim ? (y ≟ c)); + simplify;intro; + [rewrite > subst_X_apart + [reflexivity + |apply H1] + |rewrite < H + [reflexivity + |apply H1]]] +qed. + +lemma subst_X_merge : ∀M,N,x1,x2.x2 # M → + subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N. +intros 4;elim M +[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro + [rewrite > Neqb_n_n;reflexivity + |rewrite > p_eqb4 + [reflexivity + |intro;elim H;simplify;autobatch]] +|reflexivity +|simplify;simplify in H2;rewrite > H + [rewrite > H1 + [reflexivity + |intro;autobatch] + |intro;autobatch] +|simplify;rewrite > H + [reflexivity + |apply H1]] +qed. + +lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N → + subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N. +intros;elim M +[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro + [rewrite > subst_Y_not_dangling;autobatch + |reflexivity] +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro + [rewrite > p_eqb4 + [reflexivity + |assumption] + |reflexivity] +|simplify;autobatch paramodulation +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro + [reflexivity + |rewrite < H2;reflexivity]] +qed. + +inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝ +| LLPar : ∀x.LL F (Par x) +| LLApp : ∀M,N.LL F M → LL F N → LL F (App M N) +| LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) → + LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))). + +include "nat/compare.ma". + +definition max : nat → nat → nat ≝ + λx,y.match leb x y with + [ true ⇒ y + | false ⇒ x ]. + +let rec S_len M ≝ match M with +[ Par _ ⇒ O +| Var _ ⇒ O +| App N P ⇒ S (max (S_len N) (S_len P)) +| Abs x N ⇒ S (S_len N) ]. + +lemma S_len_ind : + ∀P:S_exp → Prop. + (∀M.(∀N.S_len N < S_len M → P N) → P M) + → ∀M.P M. +intros; +cut (∀N.S_len N ≤ S_len M → P N) +[|elim M 0;simplify;intros + [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch + |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max; + apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch + |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]] +apply H;intros;autobatch; +qed. + +record height : Type ≝ +{ + H : X → S_exp → Y; + HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M); + HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M; + HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false → + apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true +}. +coercion H 2. + +record xheight : Type ≝ +{ + XH : X → S_exp → Y; + XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M); + XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M; + XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false → + apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true +}. +coercion XH 2. + +include "logic/coimplication.ma". + +definition coincl : ∀A.list A → list A → Prop ≝ λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2. + +notation > "hvbox(a break ≡ b)" + non associative with precedence 45 +for @{'equiv $a $b}. + +notation < "hvbox(term 46 a break ≡ term 46 b)" + non associative with precedence 45 +for @{'equiv $a $b}. + +interpretation "list coinclusion" 'equiv x y = (coincl ? x y). + +lemma refl_coincl : ∀A.∀l:list A.l ≡ l. +intros;intro;split;intro;assumption; +qed. + +lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p. +intros;elim l1 +[reflexivity +|simplify;cases (p a);simplify;rewrite < H;reflexivity] +qed. + +lemma GV_subst_X_Var : + ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)). +intros;elim M;simplify +[cases (x ≟ c);simplify;autobatch +|autobatch +|intro;split;intro + [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2) + [cases (H x1);autobatch + |cases (H1 x1);autobatch] + |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2) + [cases (H x1);autobatch + |cases (H1 x1);autobatch]] +|intro;split;intro;cases (H x1);autobatch] +qed. + +lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M). +intros;elim M in H +[simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch +|simplify in H;elim (not_in_list_nil ?? H) +|simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch +|simplify in H1;simplify;autobatch] +qed. + +(* easy to prove, but not needed *) +lemma L_swap : ∀F:xheight.∀M.L F M → + ∀x1,x2.L F (pi_swap ? x1 x2 · M). +intros;elim H +[simplify;autobatch +|simplify;autobatch +|simplify;rewrite > pi_lemma1;simplify; + rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)) + [apply LAbs;assumption + |autobatch;]] +qed. + +lemma LL_swap : ∀F:xheight.∀M.LL F M → + ∀x1,x2.LL F (pi_swap ? x1 x2 · M). +intros;elim H +[simplify;autobatch +|simplify;autobatch +|simplify;rewrite > pi_lemma1;simplify; + rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)) + [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x)) + [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x))) + [autobatch + |elim daemon (*involution*)] + |intro;rewrite < (swap_inv ? x1 x2 c); + rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3; + rewrite < (swap_inv ? x1 x2 x);autobatch] + |autobatch]] +qed. + +(*lemma LL_subst_X : ∀F:xheight.∀M.LL F M → + ∀x1,x2.LL F (subst_X M x1 (Par x2)). +intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros +[cases (x1 ≟ c);simplify;autobatch +|inversion H1;simplify;intros;destruct +|inversion H1;simplify;intros;destruct; + clear H3 H5;apply LLApp;apply H;try assumption + [(* len *)elim daemon + |(* len *)elim daemon] +|inversion H1;simplify;intros;destruct; + unfold lam in H4;clear H3;destruct; + apply (bool_elim ? (x1 ≟ c1));intro + [rewrite > subst_X_apart + [assumption + |intro;rewrite > (?: (x1 ≟ c1) = false) in H3 + [destruct + |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1); + lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin); + apply p_eqb4;intro;rewrite > H7 in Hletin1; + rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]] + |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1)); + cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh] + clearbody c2; + rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?))) + [|rewrite > subst_X_merge + [autobatch + |intro;apply Hc2;autobatch depth=4]] + rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2))) + [|rewrite > subst_X_fp + [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?)); + rewrite > eq_swap_pi;autobatch + |intro;elim Hc2;autobatch depth=4]] + rewrite > subst_X_merge + [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4; + elim s1 0;simplify;intros + [apply (bool_elim ? (c1 ≟ c));intro; + rewrite > H6 in H5;simplify in H5; + lapply (in_list_singleton_to_eq ??? H5) + [rewrite > Hletin;autobatch + |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct] + |elim (not_in_list_nil ?? H5) + |cases (in_list_append_to_or_in_list ???? H7) + [cases (in_list_cons_case ???? (H5 H8));autobatch + |cases (in_list_cons_case ???? (H6 H8));autobatch] + |autobatch]] + rewrite > (subst_X_lemma c2 x1 ? ??) + [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2))) + [|apply p_eqb1;apply XHP; + [apply p_eqb4;intro;apply Hc2;autobatch + |simplify;rewrite > (? : (c2 ≟ x2) = false) + [reflexivity + |apply p_eqb4;intro;apply Hc2;autobatch]]] + apply LLAbs; + intros (x3); + apply H + [(*len*)elim daemon + |3:assumption + |apply H + [(*len*)elim daemon + |apply H2;intro;elim Hc2;autobatch depth=4]] + |intro;apply Hc2;autobatch + |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]] +qed.*) + +lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M. +intros;elim H +[autobatch +|autobatch +|apply LLAbs;intros;rewrite > subst_X_fp;autobatch] +qed. + +lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M. +intros;elim H +[1,2:autobatch +|apply LAbs;lapply (H2 c) + [rewrite > subst_X_x_x in Hletin;assumption + |intro;reflexivity]] +qed. + +lemma subst_X_decompose : + ∀x,y,M,N.y ∉ LV M → y ∉ E x M → + subst_X M x N = subst_Y (subst_X M x (Var y)) y N. +intros 3;elim M +[simplify;cases (x ≟ c);simplify; + [rewrite > p_eqb3;autobatch + |reflexivity] +|simplify;simplify in H; + rewrite > p_eqb4; + [reflexivity + |intro;apply H;autobatch] +|simplify;rewrite < H + [rewrite < H1 + [reflexivity + |intro;apply H2;simplify;autobatch + |intro;apply H3;simplify;autobatch] + |intro;apply H2;simplify;autobatch + |intro;apply H3;simplify;autobatch] +|simplify;apply (bool_elim ? (y ≟ c));intros; + [simplify;apply (bool_elim ? (apartb x s)) + [intro;simplify; + lapply (apartb_true_to_apart ?? H4); + rewrite > subst_X_apart + [rewrite > subst_X_apart + [reflexivity + |assumption] + |assumption] + |intro;simplify in H2;rewrite > H4 in H2; + simplify in H2;elim H2; + rewrite > (p_eqb1 ??? H3);autobatch] + |simplify;rewrite < H; + [reflexivity + |generalize in match H1;simplify;elim (LV s) + [autobatch + |intro;cases (in_list_cons_case ???? H6) + [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch + |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]] + |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro + [simplify;rewrite > E_fresh in H4 + [assumption + |autobatch] + |simplify;autobatch]]]] +qed. + +lemma subst_Y_decompose : + ∀x,y,M,N.x # M → + subst_Y M y N = subst_X (subst_Y M y (Par x)) x N. +intros 3;elim M +[simplify;simplify in H;rewrite > p_eqb4 + [reflexivity + |intro;apply H;autobatch] +|simplify;apply (bool_elim ? (y ≟ c));simplify;intro + [rewrite > Neqb_n_n;reflexivity + |reflexivity] +|simplify;rewrite < H + [rewrite < H1 + [reflexivity + |intro;apply H2;simplify;autobatch] + |intro;apply H2;simplify;autobatch] +|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro + [simplify;rewrite > subst_X_apart + [reflexivity + |assumption] + |rewrite < H + [reflexivity + |apply H1]]] +qed. + +lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M → + subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2). +intros;apply subst_X_decompose;assumption; +qed. + +lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x). +intros 3;elim M +[simplify in H;elim (not_in_list_nil ?? H); +|simplify in H;elim (not_in_list_nil ?? H) +|simplify;intro;simplify in H2;destruct; + cases (in_list_append_to_or_in_list ???? H2);autobatch +|simplify;simplify in H1; + cut (apartb x s = false) + [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro + [simplify;intro;cut (¬ x # s) + [apply Hcut1;generalize in match H3;elim s 0;simplify; + [intro;apply (bool_elim ? (x ≟ c1));simplify;intros; + [destruct + |autobatch] + |intros;autobatch + |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3) + [apply H4 + [demodulate all + |assumption] + |apply H5 + [demodulate all + |assumption]] + |intros;destruct;apply H4;demodulate all] + |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct] + |simplify;intro;apply H + [cases (in_list_cons_case ???? H1) + [rewrite > p_eqb3 in H2 + [destruct + |assumption] + |assumption] + |destruct;assumption]] + |generalize in match H1;cases (apartb x s);simplify;intro + [elim (not_in_list_nil ?? H2) + |reflexivity]]] +qed. + +let rec BV t ≝ match t with + [ Par _ ⇒ [] + | Var _ ⇒ [] + | App t1 t2 ⇒ BV t1 @ BV t2 + | Abs y u ⇒ y::BV u ]. + +lemma E_BV : ∀x,M.E x M ⊆ BV M. +intros;elim M;simplify +[1,2:unfold;intros;assumption +|unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch +|cases (apartb x s);simplify + [unfold;intros;elim (not_in_list_nil ?? H1) + |autobatch]] +qed. + +(* +let rec L_check (F:xheight) M on M ≝ match M with + [ Par _ ⇒ true + | Var _ ⇒ false + | App N P ⇒ andb (L_check F N) (L_check F P) + | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in + andb (y ≟ F X (subst_Y N y (Par X))) + (L_check F (subst_Y N y (Par X))) ]. +*) + +let rec L_check_aux (F:xheight) M n on n ≝ match n with +[ O ⇒ false (* vacuous *) +| S m ⇒ match M with + [ Par _ ⇒ true + | Var _ ⇒ false + | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m) + | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in + andb (y ≟ F X (subst_Y N y (Par X))) + (L_check_aux F (subst_Y N y (Par X)) m) ]]. + +lemma L_check_aux_sound : + ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M. +intros 2;apply (S_len_ind ?? M);intro;cases M1;intros +[autobatch +|simplify in H2;destruct +|simplify in H2;generalize in match H2; + apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n)); + apply (bool_elim ? (L_check_aux F s n));simplify;intros + [apply LApp + [apply (H ?? (pred n)) + [simplify;(*len*)elim daemon + |simplify in H1;generalize in match H1;cases n;intros + [elim (not_le_Sn_O ? H5) + |simplify;elim daemon (* H5 *)] + |(* H3 *) elim daemon] + |apply (H ?? (pred n)) + [simplify;(*len*) elim daemon + |simplify in H1;generalize in match H1;cases n;intros + [elim (not_le_Sn_O ? H5) + |simplify;elim daemon (* H5 *)] + |(* H4 *) elim daemon]] + |destruct] +|simplify in H2;generalize in match H2;clear H2; + apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))) + (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n)); + apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))); + simplify;intros + [rewrite > (p_eqb1 ??? H2); + rewrite > (? : s = + subst_X + (subst_Y s c + (Par (N_fresh X (GV s)))) + (N_fresh X (GV s)) + (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))))) + in ⊢ (?? (?? %)) + [apply LAbs;apply (H ?? (pred n)) + [simplify;(*len*)elim daemon + |simplify in H1;generalize in match H1;cases n;intros + [elim (not_le_Sn_O ? H4) + |simplify;elim daemon (* H4 *)] + |rewrite > (? : S (pred n) = n) + [assumption + |(*arith*)elim daemon]] + |rewrite < subst_Y_decompose + [rewrite < (p_eqb1 ??? H2);autobatch + |apply p_fresh]] + |destruct]] +qed. + +lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s. +intros 3;elim s +[simplify;cases (x ≟ c);simplify; + [autobatch + |unfold;intros;elim (not_in_list_nil ?? H)] +|simplify;unfold;intros;autobatch +|simplify;unfold;intros; + cases (in_list_append_to_or_in_list ???? H2) + [lapply (H ? H3);autobatch + |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin) + [applyS in_list_head + |autobatch]] +|simplify;unfold;intros; + lapply (in_list_filter ???? H1); + lapply (H ? Hletin); + cases (in_list_cons_case ???? Hletin1) + [rewrite > H2;autobatch + |apply in_list_cons;apply in_list_filter_r + [assumption + |apply (in_list_filter_to_p_true ???? H1)]]] +qed. + +lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = []. +intros 2;cases l;intro +[reflexivity +|elim (H a);autobatch] +qed. + +(* to be revised *) +lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = []. +intros;elim H +[reflexivity +|simplify;autobatch paramodulation +|simplify;generalize in match H2;generalize in match (F c s);elim s + [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro + [rewrite > p_eqb3;reflexivity + |reflexivity] + |simplify in H3;destruct + |simplify in H5;simplify; + rewrite > (? : + filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) = + filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1))) + [rewrite > H3 + [rewrite > H4 + [reflexivity + |generalize in match H5;cases (LV s2);simplify; + [intro;reflexivity + |cases (LV s1);simplify;intro;destruct]] + |generalize in match H5;cases (LV s1);simplify;intro + [reflexivity + |destruct]] + |elim (LV (subst_X s1 c (Var c1)));simplify + [reflexivity + |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]] + |simplify;apply eq_list_nil;intro;intro; + lapply (in_list_filter ???? H5) as H6; + lapply (in_list_filter ???? H6) as H7; + lapply (in_list_filter_to_p_true ???? H5) as H8; + lapply (in_list_filter_to_p_true ???? H6) as H9; + lapply (LV_subst_X ???? H7); + cut (LV s1 ⊆ [c1]) + [cases (in_list_cons_case ???? Hletin) + [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct + |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1); + rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct] + |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify + [intro;unfold;intros;elim (not_in_list_nil ?? H11) + |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros + [unfold;intros;cases (in_list_cons_case ???? H13) + [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch + |apply H11;autobatch] + |destruct]]]]] +qed. + +lemma fresh_GV_subst_X_Var : ∀s,c,y. + N_fresh X (GV (subst_X s c (Var y))) ∈ GV s → + N_fresh X (GV (subst_X s c (Var y))) = c. +intros;apply p_eqb1; +apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro +[reflexivity +|lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y)))); + lapply (GV_subst_X_Var s c y); + elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y))))); + apply H3;apply in_list_filter_r + [assumption + |change in ⊢ (???%) with (¬false);apply eq_f; + apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]] +qed. + +lemma L_check_aux_complete : + ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true. +intros 3;elim H +[reflexivity +|simplify;simplify in H5;rewrite > (? : n = S (pred n)) + [rewrite > H2 + [rewrite > H4 + [reflexivity + |(* H5 *) elim daemon] + |(* H5 *) elim daemon] + |(* H5 *) elim daemon] +|simplify;simplify in H3; + rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s))))) + (subst_Y (subst_X s c (Var (F c s))) (F c s) + (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))) + = true) + [simplify; + rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s) + (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) = + subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))) + [rewrite > (? : n = S (pred n)) + [rewrite > H2 + [reflexivity + |autobatch + |(* H3 *) elim daemon] + |(* H3 *) elim daemon] + |rewrite < subst_X_decompose + [reflexivity + |rewrite > (L_to_closed F) + [autobatch + |lapply (H1 c) + [autobatch + |intro;reflexivity]] + |autobatch]] + |rewrite < subst_X_decompose + [rewrite > subst_X_fp + [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?); + autobatch + |autobatch] + |rewrite > (L_to_closed F) + [autobatch + |lapply (H1 c) + [autobatch + |intro;reflexivity]] + |autobatch]]] +qed. + +inductive typ : Type ≝ +| TPar : X → typ +| Fun : typ → typ → typ. + +notation "hvbox(a break ▸ b)" + left associative with precedence 50 +for @{ 'blacktriangleright $a $b }. +interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b). + +include "datatypes/constructors.ma". + +definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C. + +inductive context : list (X × typ) → Prop ≝ +| ctx_nil : context [] +| ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C). + +(* ▸ = \rtrif *) +inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝ +| t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t +| t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t → + typing F C (App M N) u +| t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u → + typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u). + +inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝ +| t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t +| t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t → + typing2 F C (App M N) u +| t2_Lam : ∀C,x1,M,t,u. + (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) → + typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) → + typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u). + +notation > "C ⊢[F] M : t" + non associative with precedence 30 for @{ 'typjudg F $C $M $t }. +notation > "C ⊢ M : t" + non associative with precedence 30 for @{ 'typjudg ? $C $M $t }. +notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))" + non associative with precedence 30 for @{ 'typjudg $F $C $M $t }. +interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t). + +notation > "C ⊨[F] M : t" + non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }. +notation > "C ⊨ M : t" + non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }. +notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))" + non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }. +interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t). + +lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C. +intros 3;elim C +[elim (not_in_list_nil ?? H) +|elim (in_list_cons_case ???? H1) + [rewrite < H2;simplify;autobatch + |cases a;simplify;autobatch]] +qed. + +lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C. +intros 2;elim C +[elim (not_in_list_nil X ? H) +|elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1) + [rewrite > H2;autobatch + |cases (H H2);autobatch]] +qed. + +lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2. +intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch; +qed. + +lemma typing2_weakening : ∀F,C,M,t. + C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t. +intros 5;elim H;try autobatch size=7; +apply t2_Lam;intros;apply H2; +[intro;autobatch +|*:autobatch] +qed. + +definition swap_list : ∀N:Nset.N → N → list N → list N ≝ + λN,a,b,l.map ?? (pi_swap ? a b) l. + +lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l. +intros;elim H;simplify;autobatch; +qed. + +definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝ + λx1,x2,C.map ?? (λp. + match p with + [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C. + +lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C. +intros;generalize in match H;elim C; +[elim (not_in_list_nil ?? H1) +|simplify;inversion H2;simplify;intros;destruct;simplify;autobatch] +qed. + +lemma ctx_swap_X_swap_list : + ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C). +intros;elim C +[reflexivity +|cases a;simplify;autobatch] +qed. + +lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l. +intros;elim l;simplify;autobatch; +qed. + +lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C). +intros;elim H +[simplify;autobatch +|simplify;apply ctx_cons + [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4; + rewrite < (swap_inv ? a b); + rewrite < (swap_list_inv ? a b);autobatch + |assumption]] +qed. + +lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2. + C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t. +intros;elim H +[simplify;apply t2_axiom + [autobatch + |rewrite < eq_swap_pi;autobatch] +|simplify;autobatch +|simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam; + intros;rewrite < (swap_inv ? x1 x2 x); + change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x)); + rewrite < pi_lemma1;apply H2 + [intro;apply H3;rewrite < (swap_inv ? x1 x2 x); + rewrite > ctx_swap_X_swap_list;autobatch + |intro;rewrite > H4;autobatch]] +qed. + +lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t. +intros;elim H;try autobatch; +apply t2_Lam;intros; +rewrite > subst_X_fp +[rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l)) + [autobatch + |simplify;rewrite < eq_swap_pi;rewrite > swap_left; + rewrite < (? : l = ctx_swap_X c x2 l) + [reflexivity + |generalize in match H1;generalize in match H4;elim l 0 + [intros;reflexivity + |intro;cases a;simplify;intros; + rewrite < eq_swap_pi;rewrite > swap_other + [rewrite < H6 + [reflexivity + |*:intro;autobatch] + |*:intro;autobatch]]]] +|assumption] +qed. + +lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t. +intros;elim H;try autobatch; +generalize in match (p_fresh ? (c::DOM l@GV s)); +generalize in match (N_fresh ? (c::DOM l@GV s)); +intros (xn f_xn); +lapply (H2 xn) +[rewrite > subst_X_fp in Hletin + [lapply (t_Lam ??????? Hletin) + [intro;apply f_xn;autobatch + |rewrite < subst_X_fp in Hletin1 + [rewrite > subst_X_merge in Hletin1 + [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1 + [assumption + |rewrite > subst_X_fp + [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?)); + rewrite > eq_swap_pi;autobatch]]]]]]] +intro;elim f_xn;autobatch; +qed. \ No newline at end of file -- 2.39.2