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}}.
λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
theorem nil_cons:
- ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
- #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
+ ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+ #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))) >Heq //
qed.
(*
let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
match l1 with
[ nil ⇒ l2
- | cons hd tl ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
+ | cons hd tl ⇒ hd :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
match l with [ nil ⇒ d | cons a _ ⇒ a].
definition tail ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒ tl].
+ match l with [ nil ⇒ [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒ tl].
interpretation "append" 'append l1 l2 = (append ? l1 l2).
-theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
#A #l (elim l) normalize // qed.
theorem associative_append:
a :: (l1 @ l2) = (a :: l1) @ l2.
//; nqed. *)
-theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
+theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
#A #a #l1 #l2 >\ 5a href="cic:/matita/basics/list/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop.
- l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
+ l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
#A #l1 #l2 #P (cases l1) normalize //
#a #l3 #heq destruct
qed.
theorem nil_to_nil: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+ l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
(* iterators *)
let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
- match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
+ match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 (map A B f tl)].
lemma map_append : ∀A,B,f,l1,l2.
(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
definition filter ≝
λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
- \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.if (p x) then (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) else l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
+ \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.if (p x) then (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l0) else l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
- \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] l1.
+ \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) [ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 l1.
lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
- \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+ \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
- \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+ \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
match l1 with
[ nil ⇒ l2
- | cons a tl ⇒ rev_append S tl (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l2)
+ | cons a tl ⇒ rev_append S tl (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2)
]
.
-definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
-lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
+lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
// qed.
lemma rev_append_def : ∀S,l1,l2.
#S #l1 elim l1 normalize //
qed.
-lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
+lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
#S #a #l whd in ⊢ (??%?); //
qed.
(* an elimination principle for lists working on the tail;
useful for strings *)
lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
-(∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]))) → ∀l. P l.\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"\ 6\ 5/span\ 6
+(∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))) → ∀l. P l.
#S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/list/reverse_reverse.def(9)"\ 6reverse_reverse\ 5/a\ 6 … l)
generalize in match (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
#a #tl #H >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 @Pstep //
interpretation "norm" 'norm l = (length ? l).
lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1|\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2|.
+ |l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |l1\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|l2\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#A #l1 elim l1 // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
qed.
theorem fold_true:
∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+ \fold[op,nil]_{i ∈ a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (f a) \fold[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \fold[op,nil]_{i ∈ a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \fold[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (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.
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)} (f i).
+ \fold[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \fold[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
#A #B #a #l #p #op #nil #f elim l //
#a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa
[ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
}.
theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
- op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
+ op (\fold[op,nil]_{i∈I\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) (\fold[op,nil]_{i∈J\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \fold[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
#A #B #I #J #nil #op #f (elim I) normalize
[>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
-qed.
+qed.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
∀T1,T2:Type[0].∀l1:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1.∀l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1 → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2 → Prop.
\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l2 →
(P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?)) →
- (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl2)) →
+ (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl2)) →
P l1 l2.
#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
generalize in match Hl; generalize in match l2;
qed.
inductive in_list (A:Type[0]): A → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
-| in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))
-| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l)).
+| in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l)).
definition incl : ∀A.(\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
λA,l,m.∀x.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x m.
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.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+axiom not_in_list_nil : ∀A,x.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
(*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.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) →
+axiom in_list_cons_case : ∀A,x,a,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) →
x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
(*intros;inversion H;intros
[destruct H2;left;reflexivity
qed.*)
axiom in_list_tail : ∀l,x,y.
- \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x l.
+ \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x l.
(*intros 4;elim (in_list_cons_case ? ? ? ? H)
[elim (H2 H1)
|assumption]
qed.*)
-axiom in_list_singleton_to_eq : ∀A,x,y.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
+axiom in_list_singleton_to_eq : ∀A,x,y.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6y\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
(*intros;elim (in_list_cons_case ? ? ? ? H)
[assumption
|elim (not_in_list_nil ? ? H1)]
]
qed.
+lemma bool_elim :
+∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.∀b.(b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P b.
+#P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+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 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) x (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
match l with
- [ nil ⇒ false
+ [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
| (cons a l') ⇒
match eq x a with
- [ true ⇒ true
+ [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
| 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
(* intros 5.elim l
[simplify in H1;destruct H1
|simplify in H2;apply (bool_elim ? (equ x a))
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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l → \ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
(*intros 5.elim l
[elim (not_in_list_nil ? ? H1)
|elim H2
|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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y) →
+ ∀x,l.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → \ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#A #equ #H1 #x #l #H2
+@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 … (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l)) //
+#H3 cases H2 #H4 cases (H4 ?) @(\ 5a href="cic:/matita/cr/lambda/mem_true_to_in_list.dec"\ 6mem_true_to_in_list\ 5/a\ 6 … H3) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+lemma mem_false_to_not_in_list :
+ ∀A,equ. (∀x.equ x x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l.
+#A #equ #H1 #x #l #H2 % #H3
+>(\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ????? H3) in H2; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+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;
[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.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T B (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A B → \ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6A) (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6B).
(*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
p_fresh : ∀l.N_fresh l \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l
}.
-lemma bool_elim :
-∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.∀b.(b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P b.
-#P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
-qed.
-
lemma p_eqb3 : ∀X,x,y.x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#X #x #y @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y)) //
#H1 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H1) #H2 #H3 cases (H2 H3)
let rec GV t ≝
match t with
- [ Par x ⇒ x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
- | Var _ ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
+ [ Par x ⇒ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | Var _ ⇒ [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
| App u v ⇒ GV u \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 GV v
| Abs u ⇒ GV u ].
qed.
lemma swap_finite : ∀N,u,v.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l.∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v) x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
-#N #u #v %[@ (u\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:v\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])]
+#N #u #v %[@ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6u;v\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6]
#x #H1 @\ 5a href="cic:/matita/cr/lambda/swap_other.def(5)"\ 6swap_other\ 5/a\ 6 % #H2 cases H1 #H3 @H3 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"\ 6in_list_cons\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
qed.
*)
-definition Lam ≝ λx:\ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λM:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
+definition Lam ≝ λx:\ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λM:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
definition Judg ≝ λG,M.\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M G \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
definition body ≝ λx,M.match M with
- [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+ [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M0 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
| _ ⇒ M ].
inductive dupfree (A:Type[0]) : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
-| df_nil : dupfree A \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
-| df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl).
+| df_nil : dupfree A [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+| df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl).
record df_list (A:Type[0]) : Type[0] ≝ {
list_of_dfl :> \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A;
inductive tm : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
| tm_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
| tm_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
-| tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 x M)).
+| tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 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 : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+| tm2_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
+| tm2_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2.tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
+| tm2_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M.(∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) (\ 5a href="cic:/matita/cr/lambda/body.def(3)"\ 6body\ 5/a\ 6 x (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M)))) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 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 : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+ λx,M.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) x (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 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 : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+ λx,M.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s.
+#x #s #H1 % #H2
+lapply (\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) … 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 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s → \ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#x #s #H1 normalize
+>(\ 5a href="cic:/matita/cr/lambda/not_in_list_to_mem_false.def(4)"\ 6not_in_list_to_mem_false\ 5/a\ 6 ????? H1) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
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 \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 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 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x N \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
+#x #M elim M
+[ normalize #x0 #N #H1 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+| #n #N #H1 %
+| normalize #M1 #M2 #IH1 #IH2 #N #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+| normalize #M0 #IH #N #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
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 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 → x1 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 Q →
+ \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 P) x2 Q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x2 Q) x1 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 P x2 Q).
+#x1 #x2 #M #P #Q #H1 #H2 elim M
+[ #x0 normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H3
+ [ >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6
+ [ normalize >H3 normalize %
+ | @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+ | @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x2 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H4 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/subst_apart.def(5)"\ 6subst_apart\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ >H3 normalize %
+ ]
+| *: // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
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 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+(*
intros 3;elim M
[simplify;simplify in H;rewrite > p_eqb4
[reflexivity
|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 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M →
+ \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x2)) x2 N \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 N.
+#M #N #x1 #x2 elim M
+[normalize #x0 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H1
+ [ >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize //
+ | #H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+|#n #H1 %
+|#M1 #M2 #IH1 #IH2 normalize #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+|#M0 #IH normalize #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
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 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 →
+ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 N) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) 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.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#I #H1 elim H1 normalize
+[ #xl #x #Hx (* posn_in_elim *) @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
+| #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 *)
+ @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
+]
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:\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λxl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? pi xl.
+interpretation "apply fp list" 'middot pi xl = (fp_list pi xl).
+
+(* is it really necessary? *)
+lemma pi_no_support : ∀pi,M.\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
+#pi #M elim M
+[ normalize #x0 #H1 destruct (H1)
+| normalize //
+| #M1 #M2 #IH1 #IH2 normalize #H1 >IH1
+ [ >IH2 //
+ cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M1) in H1; normalize //
+ #x0 #xl0 #H1 destruct (H1)
+ | cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) (pi x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x.
+#pi #xl #x @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
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.pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M xl k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M) (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) k.
+#pi #M #xl elim M
+[ #x0 #k normalize >\ 5a href="cic:/matita/cr/lambda/posn_eqv.def(4)"\ 6posn_eqv\ 5/a\ 6 cases (\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t) → \ 5a href="cic:/matita/cr/lambda/tm2.ind(1,0,0)"\ 6tm2\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t).
+#xl #t #H elim H /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/tm2.con(0,1,0)"\ 6tm2_Par\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/tm2.con(0,2,0)"\ 6tm2_App\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+#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
projects / helm.git / commitdiff