From: matitaweb Date: Tue, 10 Apr 2012 17:15:10 +0000 (+0000) Subject: commit by user ricciott X-Git-Tag: make_still_working~1814 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7179a3f3e04efdfd7dee4a25416f05d03746ad26;p=helm.git commit by user ricciott --- diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index d6c066120..6dcc181f5 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -19,7 +19,7 @@ notation "hvbox(hd break :: tl)" right associative with precedence 47 for @{'cons $hd $tl}. -notation "[ list0 x sep ; ]" +notation "ref 'cons [ list0 x sep ; ref 'nil ]" non associative with precedence 90 for ${fold right @'nil rec acc @{'cons $x $acc}}. @@ -34,8 +34,8 @@ definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1 λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ]. theorem nil_cons: - ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. - #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // + ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a [a title="nil" href="cic:/fakeuri.def(1)"]/a. + #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (a:a title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq // qed. (* @@ -47,17 +47,17 @@ let rec id_list A (l: list A) on l := let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ match l1 with [ nil ⇒ l2 - | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ]. + | cons hd tl ⇒ hd :a title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ]. definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A. match l with [ nil ⇒ d | cons a _ ⇒ a]. definition tail ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. - match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒ tl]. + match l with [ nil ⇒ [a title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒ tl]. interpretation "append" 'append l1 l2 = (append ? l1 l2). -theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l. +theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l. #A #l (elim l) normalize // qed. theorem associative_append: @@ -70,24 +70,24 @@ ntheorem cons_append_commute: a :: (l1 @ l2) = (a :: l1) @ l2. //; nqed. *) -theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span +theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span #A #a #l1 #l2 >a href="cic:/matita/basics/list/associative_append.def(4)"associative_append/a // qed. theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. - l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2. + l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a[a title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2. #A #l1 #l2 #P (cases l1) normalize // #a #l3 #heq destruct qed. theorem nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. - l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. + l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a. #A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. (* iterators *) let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝ - match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)]. + match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x :a title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)]. lemma map_append : ∀A,B,f,l1,l2. (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l1) a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l2) 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 f (l1a title="append" href="cic:/fakeuri.def(1)"@/al2). @@ -101,17 +101,17 @@ let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basi definition filter ≝ λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. - a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T). + a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (x:a title="cons" href="cic:/fakeuri.def(1)":/al0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T). definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2. - a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1. + a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) [ a title="nil" href="cic:/fakeuri.def(1)"]/a l1. lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → - a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. + a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a :a title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. #A #l #a #p #pa (elim l) normalize >pa normalize // qed. lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → - a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. + a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. #A #l #a #p #pa (elim l) normalize >pa normalize // qed. theorem 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. @@ -128,13 +128,13 @@ match l1 with let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝ match l1 with [ nil ⇒ l2 - | cons a tl ⇒ rev_append S tl (aa title="cons" href="cic:/fakeuri.def(1)":/a:l2) + | cons a tl ⇒ rev_append S tl (a:a title="cons" href="cic:/fakeuri.def(1)":/al2) ] . -definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/a]. +definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l [a title="nil" href="cic:/fakeuri.def(1)"]/a. -lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). +lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a). // qed. lemma rev_append_def : ∀S,l1,l2. @@ -142,7 +142,7 @@ lemma rev_append_def : ∀S,l1,l2. #S #l1 elim l1 normalize // qed. -lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). +lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a). #S #a #l whd in ⊢ (??%?); // qed. @@ -158,7 +158,7 @@ normalize // qed. (* an elimination principle for lists working on the tail; useful for strings *) lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) → -(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))) → ∀l. P l.span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span +(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a))) → ∀l. P l. #S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l // #a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep // @@ -175,7 +175,7 @@ notation "|M|" non associative with precedence 60 for @{'norm $M}. interpretation "norm" 'norm l = (length ? l). lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. - a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="append" href="cic:/fakeuri.def(1)"@/al2| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/al1|a title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="norm" href="cic:/fakeuri.def(1)"|/al2|. + |l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="norm" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="norm" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|l2a title="norm" href="cic:/fakeuri.def(1)"|/a. #A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/ qed. @@ -205,20 +205,20 @@ interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l). theorem fold_true: ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). + \fold[op,nil]_{i ∈ a:a title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + op (f a) \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). #A #B #a #l #p #op #nil #f #pa normalize >pa // qed. theorem fold_false: ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f. -p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). +p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → \fold[op,nil]_{i ∈ a:a title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). #A #B #a #l #p #op #nil #f #pa normalize >pa // qed. theorem fold_filter: ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B. - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)} (f i). + \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + \fold[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). #A #B #a #l #p #op #nil #f elim l // #a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // @@ -233,8 +233,8 @@ record Aop (A:Type[0]) (nil:A) : Type[0] ≝ }. theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f. - op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i). + op (\fold[op,nil]_{i∈Ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) (\fold[op,nil]_{i∈Ja title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + \fold[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). #A #B #I #J #nil #op #f (elim I) normalize [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //] -qed. +qed. \ No newline at end of file diff --git a/weblib/cr/cr.ma b/weblib/cr/cr.ma new file mode 100644 index 000000000..8909dca2b --- /dev/null +++ b/weblib/cr/cr.ma @@ -0,0 +1,653 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "lambda.ma". + +(* + * beta reduction relation + * EASY TO SEE THAT BETA IS EQUIVARIANT, IMPLIES WELL-FORMEDNESS AND + * DOES NOT CREATE NEW FREE GLOBAL VARIABLES + *) +inductive beta (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| b_redex : ∀y,M,N.L F (Abs y M) → L F N → + beta F (App (Abs y M) N) (subst_Y M y N) +| b_app1 : ∀M1,M2,N.beta F M1 M2 → L F N → beta F (App M1 N) (App M2 N) +| b_app2 : ∀M,N1,N2.L F M → beta F N1 N2 → beta F (App M N1) (App M N2) +| b_xi : ∀M,N,x.beta F M N → beta F (Abs (F x M) (subst_X M x (Var (F x M)))) + (Abs (F x N) (subst_X N x (Var (F x N)))). + +(* parallel reduction relation, should have the same properties *) +inductive pr (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| pr_par : ∀x.pr F (Par x) (Par x) +| pr_redex : ∀x,M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 → + pr F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1) + (subst_X M2 x N2) +| pr_app : ∀M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 → pr F (App M1 N1) (App M2 N2) +| pr_xi : ∀M,N,x.pr F M N → pr F (Abs (F x M) (subst_X M x (Var (F x M)))) + (Abs (F x N) (subst_X N x (Var (F x N)))). + +(* complete development relation, should have the same properties *) +inductive cd (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| cd_par : ∀x.cd F (Par x) (Par x) +| cd_redex : ∀x,M1,M2,N1,N2.cd F M1 M2 → cd F N1 N2 → + cd F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1) + (subst_X M2 x N2) +| cd_app : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) → + cd F M1 M2 → cd F N1 N2 → cd F (App M1 N1) (App M2 N2) +| cd_xi : ∀M,N,x.cd F M N → cd F (Abs (F x M) (subst_X M x (Var (F x M)))) + (Abs (F x N) (subst_X N x (Var (F x N)))). + +notation < "hvbox(a break maction (>) (> \sub f) b)" + non associative with precedence 45 +for @{ 'gt $f $a $b }. +notation < "hvbox(a break maction (≫) (≫\sub f) b)" + non associative with precedence 45 +for @{ 'ggt $f $a $b }. +notation < "hvbox(a break maction (⋙) (⋙\sub f) b)" + non associative with precedence 45 +for @{ 'gggt $f $a $b }. + +notation > "hvbox(a break >[f] b)" + non associative with precedence 45 +for @{ 'gt $f $a $b }. +notation > "hvbox(a break ≫[f] b)" + non associative with precedence 45 +for @{ 'ggt $f $a $b }. +notation > "hvbox(a break ⋙[f] b)" + non associative with precedence 45 +for @{ 'gggt $f $a $b }. + +interpretation "pollack-sato beta reduction" 'gt F M N = (beta F M N). +interpretation "pollack-sato parallel reduction" 'ggt F M N = (pr F M N). +interpretation "pollack-sato complete development" 'gggt F M N = (cd F M N). + +lemma cd_exists : ∀F:xheight.∀M.L F M → ∃N.M ⋙[F] N. +intros;elim H +[autobatch +|generalize in match H2;generalize in match H1;clear H1 H2;cases s;intros + [1,2,3:cases H2;cases H4;exists [1,3,5:apply (App x x1)] + apply cd_app + [1,4,7:intros;intro;destruct + |*:assumption] + |inversion H1;simplify;intros;destruct;clear H5 H6; + cases H2;clear H2;inversion H5;simplify;intros;destruct; + cases H4;clear H4 H6;exists + [2:apply cd_redex + [3:apply H2 + |4:apply H7 + |*:skip] + |skip]] +|cases H2;clear H2;exists + [|apply cd_xi + [|apply H3]]] +qed. + +axiom pi_swap_inv : ∀u,v,M.pi_swap ? u v · (pi_swap ? u v · M) = M. + +(* useless... *) +lemma pr_swap : ∀F:xheight.∀M,N,x1,x2. + M ≫[F] N → pi_swap ? x1 x2 · M ≫[F] pi_swap ? x1 x2 · N. +intros;elim H +[simplify;autobatch +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)); + autobatch +|simplify;autobatch +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)); + [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1)); + autobatch + |autobatch]] +qed. + +inductive pr2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| pr2_par : ∀x.pr2 F (Par x) (Par x) +| pr2_redex : ∀x1,M1,M2,N1,N2. + (∀x2.(x2 ∈ GV M1 → x2 = x1) → + pr2 F (subst_X M1 x1 (Par x2)) (subst_X M2 x1 (Par x2))) → + pr2 F N1 N2 → + pr2 F (App (Abs (F x1 M1) (subst_X M1 x1 (Var (F x1 M1)))) N1) + (subst_X M2 x1 N2) +| pr2_app : ∀M1,M2,N1,N2.pr2 F M1 M2 → pr2 F N1 N2 → pr2 F (App M1 N1) (App M2 N2) +| pr2_xi : ∀M,N,x1. + (∀x2.(x2 ∈ GV M → x2 = x1) → + pr2 F (subst_X M x1 (Par x2)) (subst_X N x1 (Par x2))) → + pr2 F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) + (Abs (F x1 N) (subst_X N x1 (Var (F x1 N)))). + +inductive np (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| k1 : ∀x,M1,M2,N1,N2.np F M1 M2 → np F N1 N2 → + np F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1) + (subst_X M2 x N2). + +(*lemma np_strong_swap : ∀F:X→S_exp→Y.∀P:S_exp→S_exp→Prop. + (∀c:X. + ∀s:S_exp. + ∀s1:S_exp. + ∀s2:S_exp. + ∀s3:S_exp. + (∀x.(x ∈ GV s → x = c) → + P (subst_X s c (Par x)) (subst_X s1 c (Par x))) → + P s2 s3 → + P (App (Abs (F c s) (subst_X s c (Var (F c s)))) s2) (subst_X s1 c s3)) → + ∀s:S_exp.∀s1:S_exp.np F s s1→∀f:finite_perm X.P (f · s) (f · s1). +intros 6;elim H1;simplify; +rewrite > (?: f ·subst_X s3 c s5 = subst_X (f · s3) (f c) (f · s5)) +[rewrite > (?: f ·subst_X s2 c (Var (F c s2)) = subst_X (f · s2) (f c) (Var (F c s2))) + [rewrite > (? : F c s2 = F (f c) (f · s2)) + [apply H + [intros;rewrite > subst_X_fp [|assumption] + rewrite > subst_X_fp [|elim daemon] + [ + |apply H5] +apply H; +[intros; +|assumption]*) + +lemma pr2_swap : ∀F:xheight.∀M,N,x1,x2. + pr2 F M N → pr2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N). +intros;elim H +[simplify;autobatch +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)) + [apply pr2_redex + [intros;lapply (H2 (pi_swap ? x1 x2 x)) + [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x))); + autobatch + |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi; + apply eq_f;apply H5; + rewrite < (swap_inv ? x1 x2 x);autobatch] + |assumption] + |autobatch] +|simplify;autobatch +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)); + [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1)); + [apply pr2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x)) + [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x))); + autobatch + |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi; + apply eq_f;apply H3; + rewrite < (swap_inv ? x1 x2 x);autobatch] + |autobatch] + |autobatch]] +qed. + +(* TODO : a couple of clear but not trivial open subproofs *) +lemma pr_GV_incl : ∀F:xheight.∀M,N.M ≫[F] N → GV N ⊆ GV M. +intros;elim H;simplify +[autobatch +|cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3) + [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5)) + [apply in_list_to_in_list_append_l; + cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8; + (* reasoning from H2 and monotonicity of filter *) + elim daemon + |autobatch] + |(* boring *) elim daemon] +|unfold;intros;cases (in_list_append_to_or_in_list ???? H5);autobatch +|unfold;intros;cases (GV_subst_X_Var s c (F c s) x); + clear H4;apply H5; + cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6; + (* Hletin and monotonicity of filter *) + elim daemon] +qed. + +lemma pr_to_pr2 : ∀F:xheight.∀M,N.M ≫[F] N → pr2 F M N. +intros;elim H +[autobatch +|apply pr2_redex + [intros;rewrite > subst_X_fp + [rewrite > subst_X_fp + [autobatch + |intro;apply H5;apply pr_GV_incl; + [3,4:autobatch + |*:skip]] + |assumption] + |assumption] +|autobatch +|apply pr2_xi;intros;rewrite > subst_X_fp + [rewrite > subst_X_fp + [autobatch + |intro;apply H3;apply pr_GV_incl + [3,4:autobatch + |*:skip]] + |assumption]] +qed. + +lemma pr2_to_pr : ∀F:xheight.∀M,N.pr2 F M N → M ≫[F] N. +intros;elim H +[1,3:autobatch +|apply pr_redex + [applyS (H2 c);intro;reflexivity + |assumption] +|apply pr_xi;applyS (H2 c);intro;reflexivity] +qed. + +(* ugly, must factorize *) +lemma pr_subst_X : ∀F:xheight.∀M1,M2,x,N1,N2. + M1 ≫[F] M2 → N1 ≫[F] N2 → + subst_X M1 x N1 ≫[F] subst_X M2 x N2. +intros;lapply (pr_to_pr2 ??? H) as H';clear H; +generalize in match H1;generalize in match N2 as N2;generalize in match N1 as N1; +clear H1 N1 N2; +elim H' +[simplify;apply (bool_elim ? (x ≟ c));simplify;intro;autobatch +|generalize in match (p_fresh ? (x::GV s @GV N1)); + generalize in match (N_fresh ??); + intros (c1 Hc1); + rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) = + Abs (F c1 (pi_swap ? c c1 · s)) + (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s))))) + [rewrite > (?: subst_X s1 c s3 = subst_X (pi_swap ? c c1 · s1) c1 s3) + [simplify;rewrite > subst_X_lemma + [rewrite > subst_X_lemma in ⊢ (???%) + [rewrite > (?: F c1 (pi_swap ? c c1 · s) = + F c1 (subst_X (pi_swap ? c c1 · s) x N1)) + [simplify in ⊢ (? ? (? (? ? (? ? ? %)) ?) ?);apply pr_redex + [rewrite < subst_X_fp + [rewrite < subst_X_fp + [apply H1 + [intro Hfalse;elim Hc1;autobatch + |assumption] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l; + lapply (H c) [|intro;reflexivity] + lapply (pr2_to_pr ??? Hletin); + do 2 rewrite > subst_X_x_x in Hletin1; + apply (pr_GV_incl ??? Hletin1);assumption] + |intro Hfalse;elim Hc1;autobatch] + |autobatch] + |apply p_eqb1;apply XHP + [apply p_eqb4;intro Hfalse;apply Hc1;rewrite > Hfalse;autobatch + |apply apart_to_apartb_true;unfold;autobatch]] + |*:intro Hfalse;autobatch] + |*:intro Hfalse;autobatch] + |rewrite < subst_X_fp + [rewrite > subst_X_merge + [reflexivity + |intro Hfalse;autobatch] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l; + lapply (H c) [|intro;reflexivity] + do 2 rewrite > subst_X_x_x in Hletin; + lapply (pr2_to_pr ??? Hletin);autobatch]] + |rewrite < (swap_left ? c c1) in ⊢ (? ? ? (? (??%?) (? ? % (? (? ? % ?))))); + rewrite > eq_swap_pi;rewrite < XHE; + change in ⊢ (???(??(???%))) with (pi_swap ? c c1 · (Var (F c s))); + rewrite < pi_lemma1;rewrite < subst_X_fp + [rewrite > (subst_X_apart ?? (Par c1)) + [reflexivity + |elim daemon (* don't we have a lemma? *)] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]] +|simplify;autobatch +|generalize in match (p_fresh ? (x::GV s @GV N1)); + generalize in match (N_fresh ??); + intros (c1 Hc1); + rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) = + Abs (F c1 (pi_swap ? c c1 · s)) + (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s))))); + [rewrite > (?: Abs (F c s1) (subst_X s1 c (Var (F c s1))) = + Abs (F c1 (pi_swap ? c c1 · s1)) + (subst_X (pi_swap ? c c1 · s1) c1 (Var (F c1 (pi_swap ? c c1 · s1))))); + [simplify;rewrite > subst_X_lemma + [rewrite > subst_X_lemma in ⊢ (???%) + [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N1)) + [rewrite > (? : F c1 (pi_swap ? c c1 · s1) = F c1 (subst_X (pi_swap ? c c1 · s1) x N2)) + [apply pr_xi;rewrite < subst_X_fp + [rewrite < subst_X_fp + [apply H1 + [intro Hfalse;elim Hc1;autobatch + |assumption] + |intro Hfalse; (* meglio fare qualcosa di più furbo *) elim daemon] + |intro;elim Hc1;autobatch] + |apply p_eqb1;apply XHP + [apply p_eqb4;intro Hfalse;autobatch + |apply apart_to_apartb_true;intro;autobatch]] + |apply p_eqb1;apply XHP + [apply p_eqb4;intro Hfalse;autobatch + |apply apart_to_apartb_true;intro;autobatch]] + |*:intro;apply Hc1;autobatch] + |*:intro;apply Hc1;autobatch] + |apply eq_f2 + [autobatch + |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?)))); + rewrite > eq_swap_pi;rewrite < XHE; + change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s1))); + rewrite < pi_lemma1;rewrite < subst_X_fp + [rewrite > (subst_X_apart ?? (Par c1)) + [reflexivity + |elim daemon (* don't we have a lemma? *)] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]] + |apply eq_f2 + [autobatch + |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?)))); + rewrite > eq_swap_pi;rewrite < XHE; + change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s))); + rewrite < pi_lemma1;rewrite < subst_X_fp + [rewrite > (subst_X_apart ?? (Par c1)) + [reflexivity + |elim daemon (* don't we have a lemma? *)] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]]] +qed. + +lemma L_subst_X : ∀F:xheight.∀M,x,N.L F M → L F N → L F (subst_X M x N). +intros;elim (L_to_LL ?? H); +[simplify;cases (x ≟ c);simplify;autobatch +|simplify;autobatch +|generalize in match (p_fresh ? (x::GV s @GV N)); + generalize in match (N_fresh ??); + intros (c1 Hc1); + rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) = + Abs (F c1 (pi_swap ? c c1 · s)) + (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s))))); + [simplify;rewrite > subst_X_lemma + [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N)) + [apply LAbs;rewrite < subst_X_fp + [apply H3;intro Hfalse;elim Hc1;autobatch + |intro Hfalse;elim Hc1;autobatch] + |apply p_eqb1;apply XHP + [apply p_eqb4;intro Hfalse;autobatch + |apply apart_to_apartb_true;intro;autobatch]] + |*:intro;apply Hc1;autobatch] + |apply eq_f2 + [autobatch + |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?)))); + rewrite > eq_swap_pi;rewrite < XHE; + change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s))); + rewrite < pi_lemma1;rewrite < subst_X_fp + [rewrite > (subst_X_apart ?? (Par c1)) + [reflexivity + |elim daemon (* don't we have a lemma? *)] + |intro Hfalse;elim Hc1; + apply in_list_cons;apply in_list_to_in_list_append_l; + (* lemma?? *) elim daemon]]]] +qed. + +inductive cd2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝ +| cd2_par : ∀x.cd2 F (Par x) (Par x) +| cd2_redex : ∀x,M1,M2,N1,N2. + (∀x2.(x2 ∈ GV M1 → x2 = x) → + cd2 F (subst_X M1 x (Par x2)) (subst_X M2 x (Par x2))) → + cd2 F N1 N2 → + cd2 F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1) + (subst_X M2 x N2) +| cd2_app : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) → + cd2 F M1 M2 → cd2 F N1 N2 → cd2 F (App M1 N1) (App M2 N2) +| cd2_xi : ∀M,N,x.(∀x2.(x2 ∈ GV M → x2 = x) → + cd2 F (subst_X M x (Par x2)) (subst_X N x (Par x2))) → + cd2 F (Abs (F x M) (subst_X M x (Var (F x M)))) + (Abs (F x N) (subst_X N x (Var (F x N)))). + +lemma cd2_swap : ∀F:xheight.∀M,N,x1,x2. + cd2 F M N → cd2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N). +intros;elim H +[simplify;autobatch +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)) + [apply cd2_redex + [intros;lapply (H2 (pi_swap ? x1 x2 x)) + [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x))); + autobatch + |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi; + apply eq_f;apply H5; + rewrite < (swap_inv ? x1 x2 x);autobatch] + |assumption] + |autobatch] +|simplify;apply cd2_app; + [intros;generalize in match H1;cases s;simplify;intros 2;destruct; + elim H6;[3:reflexivity|*:skip] + |*:assumption] +|simplify;do 2 rewrite > pi_lemma1;simplify; + rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s)); + [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1)); + [apply cd2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x)) + [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x))); + autobatch + |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi; + apply eq_f;apply H3; + rewrite < (swap_inv ? x1 x2 x);autobatch] + |autobatch] + |autobatch]] +qed. + +lemma cd_GV_incl : ∀F:xheight.∀M,N.M ⋙[F] N → GV N ⊆ GV M. +intros;elim H;simplify +[autobatch +|cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3) + [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5)) + [apply in_list_to_in_list_append_l; + cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8; + (* reasoning from H2 and monotonicity of filter *) + elim daemon + |autobatch] + |(* boring *) elim daemon] +|unfold;intros;cases (in_list_append_to_or_in_list ???? H6);autobatch +|unfold;intros;cases (GV_subst_X_Var s c (F c s) x); + clear H4;apply H5; + cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6; + (* Hletin and monotonicity of filter *) + elim daemon] +qed. + +lemma cd_to_cd2 : ∀F:xheight.∀M,N.M ⋙[F] N → cd2 F M N. +intros;elim H +[autobatch +|apply cd2_redex + [intros;rewrite > subst_X_fp + [rewrite > subst_X_fp + [autobatch + |intro;apply H5;apply cd_GV_incl; + [3,4:autobatch + |*:skip]] + |assumption] + |assumption] +|autobatch +|apply cd2_xi;intros;rewrite > subst_X_fp + [rewrite > subst_X_fp + [autobatch + |intro;apply H3;apply cd_GV_incl + [3,4:autobatch + |*:skip]] + |assumption]] +qed. + +lemma pr_cd_triangle : ∀F:xheight.∀M,N,P.M ≫[F] N → M ⋙[F] P → N ≫[F] P. +intros;generalize in match H;generalize in match N;clear H N; +elim (cd_to_cd2 ??? H1) +[inversion H;simplify;intros;destruct;autobatch +|inversion (pr_to_pr2 ??? H5);simplify;intros;destruct; + [clear H7 H9; + lapply (H4 ? (pr2_to_pr ??? H8)) as H9;clear H4; + generalize in match (p_fresh ? (GV s)); + generalize in match (N_fresh ? (GV s));intros; + rewrite > (? : subst_X s6 c1 s8 = subst_X (subst_X s6 c1 (Par c2)) c2 s8) + [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3) + [apply pr_subst_X + [apply H2; + [intro;elim H4;assumption + |rewrite > (? : subst_X s c (Par c2) = subst_X s5 c1 (Par c2)) + [apply pr2_to_pr;apply H6;intro; (* must be fresh in s5 *) elim daemon + |(* by Hcut2 *) elim daemon]] + |assumption] + |(* as long as it's fresh in s1 too *) elim daemon] + |(* as long as it's fresh in s6 too *) elim daemon] + |lapply (H4 ? (pr2_to_pr ??? H8));inversion H6;intros;simplify;destruct; + clear H11 H7 H9; + generalize in match (p_fresh ? (GV s)); + generalize in match (N_fresh ? (GV s));intros; + rewrite > (? : subst_X s5 c1 (Var (F c1 s5)) = subst_X (subst_X s5 c1 (Par c2)) c2 (Var (F c1 s5))) + [rewrite > (? : F c1 s5 = F c2 (subst_X s5 c1 (Par c2))) + [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3) + [apply pr_redex + [apply H2 + [intro;elim H7;assumption + |rewrite > (?: subst_X s c (Par c2) = subst_X s4 c1 (Par c2)) + [apply pr2_to_pr;apply H10;(* suff fresh *) elim daemon + |(* by Hcut1 *) elim daemon]] + |assumption] + |(* suff. fresh *) elim daemon] + |(* eqvariance *) elim daemon] + |(* eqvariance *) elim daemon]] +|inversion H6;simplify;intros;destruct; + [elim H [3:reflexivity|*:skip] + |autobatch] +|inversion (pr_to_pr2 ??? H3);simplify;intros;destruct;clear H5; + generalize in match (p_fresh ? (GV s)); + generalize in match (N_fresh ? (GV s));intros; + rewrite > (?: subst_X s4 c1 (Var (F c1 s4)) = subst_X (subst_X s4 c1 (Par c2)) c2 (Var (F c1 s4))) + [rewrite > (?: subst_X s1 c (Var (F c s1)) = subst_X (subst_X s1 c (Par c2)) c2 (Var (F c s1))) + [rewrite > (?: F c1 s4 = F c2 (subst_X s4 c1 (Par c2))) + [rewrite > (?: F c s1 = F c2 (subst_X s1 c (Par c2))) + [apply pr_xi;apply H2 + [intro;elim H5;assumption + |rewrite > (?: subst_X s c (Par c2) = subst_X s3 c1 (Par c2)) + [apply pr2_to_pr;apply H4;(*suff. fresh*) elim daemon + |(*by Hcut1*)elim daemon]] + |(*perm*)elim daemon] + |(*perm*)elim daemon] + |(*suff.fresh*) elim daemon] + |(*suff.fresh*) elim daemon]] + qed. + +lemma diamond_pr : ∀F:xheight.∀a,b,c.a ≫[F] b → a ≫[F] c → + ∃d.b ≫[F] d ∧ c ≫[F] d. +intros; +cut (L F a) +[cases (cd_exists ?? Hcut) (d); + exists[apply d] + split;autobatch; +|elim H;autobatch] +qed. + +inductive tc (A:Type) (R:A → A → Prop) : A → A → Prop ≝ +| tc_refl : ∀x:A.tc A R x x +| tc_trans : ∀x,y,z.R x y → tc A R y z → tc A R x z. + +lemma strip_tc_pr : ∀F:xheight.∀a,b,c.pr F a b → tc ? (pr F) a c → + ∃d.tc ? (pr F) b d ∧ pr F c d. +intros;generalize in match H;generalize in match b;clear H b;elim H1 +[autobatch; +|cases (diamond_pr ???? H H4);cases H5;clear H5; + cases (H3 ? H6);cases H5;clear H5;exists[apply x1] + split;autobatch] +qed. + +lemma diamond_tc_pr : ∀F:xheight.∀a,b,c.tc ? (pr F) a b → tc ? (pr F) a c → + ∃d.tc ? (pr F) b d ∧ tc ? (pr F) c d. +intros 5;generalize in match c; clear c;elim H +[autobatch; +|cases (strip_tc_pr ???? H1 H4);cases H5;clear H5; + cases (H3 ? H6);cases H5;clear H5; + exists[apply x1] + split;autobatch] +qed. + +lemma tc_split : ∀A,R,a,b,c.tc A R a b → tc A R b c → tc A R a c. +intros 6;elim H;autobatch; +qed. + +lemma tc_single : ∀A,R,a,b.R a b → tc A R a b. +intros;autobatch; +qed. + +lemma tcb_app1 : ∀F:xheight.∀M1,M2,N.tc ? (beta F) M1 M2 → L F N → + tc ? (beta F) (App M1 N) (App M2 N). +intros;elim H;autobatch; +qed. + +lemma tcb_app2 : ∀F:xheight.∀M,N1,N2.L F M → tc ? (beta F) N1 N2 → + tc ? (beta F) (App M N1) (App M N2). +intros;elim H1;autobatch; +qed. + +lemma tcb_xi : ∀F:xheight.∀M,N,x. + tc ? (beta F) M N → + tc ? (beta F) (Abs (F x M) (subst_X M x (Var (F x M)))) + (Abs (F x N) (subst_X N x (Var (F x N)))). +intros;elim H;autobatch; +qed. + +lemma red_lemma : + ∀F:xheight.∀x,M,N.L F M → + subst_X M x N = subst_Y (subst_X M x (Var (F x M))) (F x M) N. +intros;rewrite < subst_X_decompose; +[reflexivity +|rewrite > L_to_closed;autobatch +|autobatch] +qed. + +lemma b_redex2 : + ∀F:xheight.∀x,M,N.L F M → L F N → + beta F (App (Abs (F x M) (subst_X M x (Var (F x M)))) N) (subst_X M x N). +intros;rewrite > (red_lemma ???? H) in ⊢ (???%); +apply b_redex;autobatch; +qed. + +lemma pr_to_L_1 : ∀F:xheight.∀a,b.a ≫[F] b → L F a. +intros;elim H;autobatch; +qed. + +lemma pr_to_L_2 : ∀F:xheight.∀a,b.a ≫[F] b → L F b. +intros;elim H;autobatch; +qed. + +lemma pr_to_tc_beta : ∀F:xheight.∀a,b.a ≫[F] b → tc ? (beta F) a b. +intros;elim H +[autobatch +|apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s) (subst_X s c (Var (F c s)))) s3) ?)); + [apply tcb_app2;autobatch + |apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s1) (subst_X s1 c (Var (F c s1)))) s3) ?)); + [apply tcb_app1;autobatch + |apply tc_single;apply b_redex2;autobatch]] +|apply (tc_split ????? (?: tc ?? (App s s2) (App s s3))) + [apply tcb_app2;autobatch + |apply tcb_app1;autobatch] +|autobatch] +qed. + +lemma pr_refl : ∀F:xheight.∀a.L F a → a ≫[F] a. +intros;elim H;try autobatch; +qed. + +lemma tc_pr_to_tc_beta: ∀F:xheight.∀a,b.tc ? (pr F) a b → tc ? (beta F) a b. +intros;elim H;autobatch; +qed. + +lemma beta_to_pr : ∀F:xheight.∀a,b.a >[F] b → a ≫[F] b. +intros;elim H +[inversion H1;intros;destruct; + rewrite < subst_X_decompose + [autobatch + |rewrite > (L_to_closed ?? H3);autobatch + |autobatch] +|2,3:apply pr_app;autobatch +|apply pr_xi;assumption] +qed. + +lemma tc_beta_to_tc_pr: ∀F:xheight.∀a,b.tc ? (beta F) a b → tc ? (pr F) a b. +intros;elim H;autobatch; +qed. + +theorem church_rosser: + ∀F:xheight.∀a,b,c.tc ? (beta F) a b → tc ? (beta F) a c → + ∃d.tc ? (beta F) b d ∧ tc ? (beta F) c d. +intros;lapply (tc_beta_to_tc_pr ??? H);lapply (tc_beta_to_tc_pr ??? H1); +cases (diamond_tc_pr ???? Hletin Hletin1);cases H2; +exists[apply x] +split;autobatch; +qed. \ No newline at end of file diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma index f368613c7..a5c769a38 100644 --- a/weblib/cr/lambda.ma +++ b/weblib/cr/lambda.ma @@ -57,7 +57,7 @@ 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)) → + (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/atl1) (hd2a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/atl2)) → P l1 l2. #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons generalize in match Hl; generalize in match l2; @@ -92,8 +92,8 @@ lemma length_append : ∀A,l,m.a href="cic:/matita/basics/list/length.fix(0,1,1 qed. inductive in_list (A:Type[0]): A → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝ -| in_list_head : ∀ x,l.(in_list A x (xa title="cons" href="cic:/fakeuri.def(1)":/a:l)) -| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l)). +| in_list_head : ∀ x,l.(in_list A x (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al)) +| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (ya title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al)). definition incl : ∀A.(a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝ λA,l,m.∀x.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x m. @@ -105,13 +105,13 @@ interpretation "list member" 'mem x l = (in_list ? x l). interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). -axiom not_in_list_nil : ∀A,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x a title="nil" href="cic:/fakeuri.def(1)"[/a]. +axiom not_in_list_nil : ∀A,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x [a title="nil" href="cic:/fakeuri.def(1)"]/a. (*intros.unfold.intro.inversion H [intros;lapply (sym_eq ? ? ? H2);destruct Hletin |intros;destruct H4] qed.*) -axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) → +axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l. (*intros;inversion H;intros [destruct H2;left;reflexivity @@ -119,13 +119,13 @@ axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind( qed.*) axiom in_list_tail : ∀l,x,y. - a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l) → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x l. + a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x (ya title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x l. (*intros 4;elim (in_list_cons_case ? ? ? ? H) [elim (H2 H1) |assumption] qed.*) -axiom in_list_singleton_to_eq : ∀A,x,y.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y. +axiom in_list_singleton_to_eq : ∀A,x,y.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x a title="cons" href="cic:/fakeuri.def(1)"[/aya title="nil" href="cic:/fakeuri.def(1)"]/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y. (*intros;elim (in_list_cons_case ? ? ? ? H) [assumption |elim (not_in_list_nil ? ? H1)] @@ -161,22 +161,25 @@ lemma in_list_append_elim: ] qed. +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. -(* -let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ +let rec mem (A:Type[0]) (eq: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) x (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ match l with - [ nil ⇒ false + [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | (cons a l') ⇒ match eq x a with - [ true ⇒ true + [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ mem A eq x l' ] ]. -naxiom mem_true_to_in_list : - \forall A,equ. - (\forall x,y.equ x y = true \to x = y) \to - \forall x,l.mem A equ x l = true \to in_list A x l. +axiom mem_true_to_in_list : + ∀A,equ. + (∀x,y.equ 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) → + ∀x,l.a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l. (* intros 5.elim l [simplify in H1;destruct H1 |simplify in H2;apply (bool_elim ? (equ x a)) @@ -185,10 +188,10 @@ naxiom mem_true_to_in_list : 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. +axiom in_list_to_mem_true : + ∀A,equ. + (∀x.equ x x 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,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l → a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. (*intros 5.elim l [elim (not_in_list_nil ? ? H1) |elim H2 @@ -196,8 +199,24 @@ naxiom in_list_to_mem_true : |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. +lemma not_in_list_to_mem_false : + ∀A,equ. (∀x,y.equ 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) → + ∀x,l.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#A #equ #H1 #x #l #H2 +@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a … (a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l)) // +#H3 cases H2 #H4 cases (H4 ?) @(a href="cic:/matita/cr/lambda/mem_true_to_in_list.dec"mem_true_to_in_list/a … H3) /span class="autotactic"2span class="autotrace" trace /span/span/ +qed. + +lemma mem_false_to_not_in_list : + ∀A,equ. (∀x.equ x x 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,l.a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l 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="list not member" href="cic:/fakeuri.def(1)"∉/a l. +#A #equ #H1 #x #l #H2 % #H3 +>(a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"in_list_to_mem_true/a ????? H3) in H2; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ +qed. + +(* +axiom in_list_filter_to_p_true : ∀A,l,x,p. +in_list A x (filter A l p) → 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; @@ -229,26 +248,24 @@ naxiom in_list_filter_r : \forall A,l,p,x. [apply in_list_cons;apply H;assumption |apply H;assumption]]] qed.*) +*) -naxiom incl_A_A: ∀T,A.incl T A A. +axiom incl_A_A: ∀T,A.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A A. (*intros.unfold incl.intros.assumption. qed.*) -naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). +axiom incl_append_l : ∀T,A,B.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A (A a title="append" href="cic:/fakeuri.def(1)"@/a B). (*unfold incl; intros;autobatch. qed.*) -naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). +axiom incl_append_r : ∀T,A,B.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T B (A a title="append" href="cic:/fakeuri.def(1)"@/a B). (*unfold incl; intros;autobatch. qed.*) -naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +axiom incl_cons : ∀T,A,B,x.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A B → a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T (x:a title="cons" href="cic:/fakeuri.def(1)":/aA) (x:a title="cons" href="cic:/fakeuri.def(1)":/aB). (*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 @@ -262,11 +279,6 @@ record Nset : Type[1] ≝ 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) @@ -356,8 +368,8 @@ let rec vclose t xl k on t ≝ 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] + [ Par x ⇒ a title="cons" href="cic:/fakeuri.def(1)"[/axa 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 ]. @@ -479,7 +491,7 @@ lemma swap_surj : ∀N,u,v.a href="cic:/matita/basics/relations/surjective.def( 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])] +#N #u #v %[@ a title="cons" href="cic:/fakeuri.def(1)"[/au;va 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. @@ -653,17 +665,17 @@ intros;elim M 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 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 a title="cons" href="cic:/fakeuri.def(1)"[/axa 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 + [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M0 a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | _ ⇒ M ]. inductive dupfree (A:Type[0]) : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝ -| df_nil : dupfree A a title="nil" href="cic:/fakeuri.def(1)"[/a] -| df_cons : ∀x,xl.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → dupfree A xl → dupfree A (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl). +| df_nil : dupfree A [a title="nil" href="cic:/fakeuri.def(1)"]/a +| df_cons : ∀x,xl.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → dupfree A xl → dupfree A (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/axl). record df_list (A:Type[0]) : Type[0] ≝ { list_of_dfl :> a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A; @@ -674,283 +686,68 @@ record df_list (A:Type[0]) : Type[0] ≝ { inductive tm : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ | tm_Par : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.x a title="list member" href="cic:/fakeuri.def(1)"∈/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x)) | tm_App : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M1,M2:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M1) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M2) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2)) -| tm_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.∀M:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl) M) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/Lam.def(5)"Lam/a x M)). +| tm_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.∀M:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/axl) M) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/Lam.def(5)"Lam/a x M)). - -inductive tm2 : pre_tm → Prop ≝ -| tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x)) -| tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2)) -| tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs 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)). +(* I see no point in using cofinite quantification here *) +inductive tm2 : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ +| tm2_Par : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.x a title="list member" href="cic:/fakeuri.def(1)"∈/a xl → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x)) +| tm2_App : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M1,M2.tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M1) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M2) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2)) +| tm2_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M.(∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (x:a title="cons" href="cic:/fakeuri.def(1)":/axl) (a href="cic:/matita/cr/lambda/body.def(3)"body/a x (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M)))) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a 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. +definition apartb : a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝ + λx,M.a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a a href="cic:/matita/cr/lambda/X.dec"X/a (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a a href="cic:/matita/cr/lambda/X.dec"X/a) x (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a 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. +definition apart : a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ + λx,M.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M. -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. +interpretation "name apartness wrt GV" 'apart x s = (apart x s). -lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M). -intros;reflexivity; +lemma apartb_true_to_apart : ∀x,s.a href="cic:/matita/cr/lambda/apartb.def(3)"apartb/a x s 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="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a s. +#x #s #H1 % #H2 +lapply (a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"in_list_to_mem_true/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a a href="cic:/matita/cr/lambda/X.dec"X/a) … H2) // +#Hletin normalize in H1; >Hletin in H1; +normalize #Hfalse destruct (Hfalse) 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] +lemma apart_to_apartb_true : ∀x,s.x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a s → a href="cic:/matita/cr/lambda/apartb.def(3)"apartb/a x s 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 #s #H1 normalize +>(a href="cic:/matita/cr/lambda/not_in_list_to_mem_false.def(4)"not_in_list_to_mem_false/a ????? H1) /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 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]]] +lemma pi_Abs : ∀pi,M.pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a 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 a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a M). +#pi #M % 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]]] +lemma subst_apart : ∀x,M,N. x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M → a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x N a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M. +#x #M elim M +[ normalize #x0 #N #H1 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a/span/span/ +| #n #N #H1 % +| normalize #M1 #M2 #IH1 #IH2 #N #H1 >IH1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_l.dec"incl_append_l/a/span/span/ >IH2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_r.dec"incl_append_r/a/span/span/ +| normalize #M0 #IH #N #H1 >IH /span class="autotactic"3span class="autotrace" trace /span/span/ +] 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] +lemma subst_lemma : + ∀x1,x2,M,P,Q.x1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x2 → x1 a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a Q → + a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 P) x2 Q a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x2 Q) x1 (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a P x2 Q). +#x1 #x2 #M #P #Q #H1 #H2 elim M +[ #x0 normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x1 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H3 + [ >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a + [ normalize >H3 normalize % + | @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) /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 ? (x2 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H4 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/subst_apart.def(5)"subst_apart/a/span/span/ + >H3 normalize % + ] +| *: // normalize /span class="autotactic"2span class="autotrace" trace /span/span/ +] qed. -lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y). +(* was: subst_cancel *) +(* won't prove it now because it's unsure if we need a more general version, + with a list xl instead of [x], and/or with a generic n instead of O *) +axiom vopen_vclose_cancel : ∀x,M.x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M → M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a (a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +(* intros 3;elim M [simplify;simplify in H;rewrite > p_eqb4 [reflexivity @@ -972,749 +769,85 @@ intros 3;elim M |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. +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] +lemma subst_merge : ∀M,N,x1,x2.x2 a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M → + a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x2)) x2 N a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 N. +#M #N #x1 #x2 elim M +[normalize #x0 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x1 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H1 + [ >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize // + | #H2 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a/span/span/ + ] +|#n #H1 % +|#M1 #M2 #IH1 #IH2 normalize #H1 >IH1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_l.dec"incl_append_l/a/span/span/ >IH2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_r.dec"incl_append_r/a/span/span/ +|#M0 #IH normalize #H1 >IH /span class="autotactic"3span class="autotrace" trace /span/span/ +] 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. +(* was: subst_X_Y_commute + won't prove it now, it's not easy to understand if it's needed and in which form *) +axiom subst_vopen_commute : ∀x1,x2,M,N. x1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x2 → + a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 N) a title="cons" href="cic:/fakeuri.def(1)"[/ax2a title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M a title="cons" href="cic:/fakeuri.def(1)"[/ax2a title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) x1 N. -(* 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. +axiom daemon : ∀P:Prop.P. -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]] +lemma GV_tm_nil : ∀I.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a I → a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a I a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a. +#I #H1 elim H1 normalize +[ #xl #x #Hx (* posn_in_elim *) @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a +| #xl #M1 #M2 #H1 #H2 #IH1 #IH2 >IH1 >IH2 % +| #xl #x #M #H1 #H2 #IH1 + (* prove vclose (vclose M xl n) yl |xl| = vclose M (xl@yl) n *) + @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a +] 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] +definition fp_list ≝ λpi:a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a.λxl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a a href="cic:/matita/cr/lambda/X.dec"X/a.a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? pi xl. +interpretation "apply fp list" 'middot pi xl = (fp_list pi xl). + +(* is it really necessary? *) +lemma pi_no_support : ∀pi,M.a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aM a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M. +#pi #M elim M +[ normalize #x0 #H1 destruct (H1) +| normalize // +| #M1 #M2 #IH1 #IH2 normalize #H1 >IH1 + [ >IH2 // + cases (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M1) in H1; normalize // + #x0 #xl0 #H1 destruct (H1) + | cases (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M1) in H1; // + #x0 #xl0 normalize #H1 destruct (H1) + ] +| normalize #M0 #IH0 #H1 >IH0 // +] 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]] +lemma posn_eqv : ∀pi,xl,x.a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? (pia title="apply fp list" href="cic:/fakeuri.def(1)"·/axl) (pi x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? xl x. +#pi #xl #x @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a 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]]]] +lemma vclose_eqv : ∀pi,M,xl,k.pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M xl k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a (pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aM) (pia title="apply fp list" href="cic:/fakeuri.def(1)"·/axl) k. +#pi #M #xl elim M +[ #x0 #k normalize >a href="cic:/matita/cr/lambda/posn_eqv.def(4)"posn_eqv/a cases (a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a a href="cic:/matita/cr/lambda/X.dec"X/a xl x0) normalize // +| #n0 #k % +| #M1 #M2 #IH1 #IH2 #k whd in ⊢ (??%%); // +| #M0 #IH0 #k whd in ⊢ (??%%); // +] 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 tm_eqv : ∀pi,I.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a I → pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aI a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a I. +#pi #I #H1 elim H1 +[ #xl0 #x0 #Hx0 -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. +theorem term_to_term2 : ∀xl,t.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl t) → a href="cic:/matita/cr/lambda/tm2.ind(1,0,0)"tm2/a (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl t). +#xl #t #H elim H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/tm2.con(0,1,0)"tm2_Par/a, a href="cic:/matita/cr/lambda/tm2.con(0,2,0)"tm2_App/a/span/span/ +#xl0 #x0 #M #Hx #H1 #IH1 %3 #x1 #Hx1 +normalize in ⊢ (?(??%)); -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. +1) dimostrare che GV di un term judgment (debole) è vuoto +2) dimostrare che pi*T = T se GV(T) = [] +3) term judgment forte -> term judgment debole +4) allora per 1+2 => term judgment equivariante (entrambi) +5) 4) => term judgment debole -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 +*) \ No newline at end of file