New notation for congruence

[helm.git] / matita / matita / lib / turing / universal / tuples.ma

diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 6e09b9d5217c61b1ed31c8e20c346c2402256e29..9207b8582fafb0a47f0bf195a91ab512ad74a264 100644 (file)
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -85,8 +85,6 @@ axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
     (∃q.|l1| = (tuple_length (S n))*q) ∧ 
       tuple_TM (S n) (mk_tuple qin cin qout cout mv).
 
-axiom daemon: ∀P:Prop. P.
-
 lemma match_to_tuples_list: ∀n,h,l,qin,cin,qout,cout,mv.
   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) → 
     ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_list n h l).
@@ -95,7 +93,8 @@ lemma match_to_tuples_list: ∀n,h,l,qin,cin,qout,cout,mv.
 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
 @(flatten_to_mem … Hflat … Hlen)  
   [// 
-  |@daemon
+  |#x #memx @length_of_tuple 
+   cases (mem_map ????? memx) #t * #memt #Ht <Ht // 
   |@(length_of_tuple … Htuple) 
   ]
 qed.
@@ -124,8 +123,8 @@ qed.
 
 lemma trans_to_match:
   ∀n.∀h.∀trans: trans_source n → trans_target n.
-  ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp →
-  tuple_encoding n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
+  ∀s,t,qin,cin,qout,cout,mv. trans s = t →
+  tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv →
   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))).
 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple 
 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward 
@@ -133,18 +132,37 @@ lemma trans_to_match:
 @graph_enum_complete //
 qed.
 
+(*
 axiom append_eq_tech1 :
   ∀A,l1,l2,l3,l4.l1@l2 = l3@l4 → |l1| < |l3| → ∃la:list A.l1@la = l3.
 axiom append_eq_tech2 :
   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false → ∃la:list A.l3 = l1@a::la.
-(*axiom list_decompose_cases : 
+axiom list_decompose_cases : 
   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → ∃la,lb:list A.l3 = la@a::lb ∨ l4 = la@a::lb.
 axiom list_decompose_l :
   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false → 
   ∃la,lb.l2 = la@lb ∧ l3 = l1@a::la.*)
-axiom list_decompose_r :
+  
+lemma list_decompose_r :
   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l3 = false → 
   ∃la,lb.l1 = la@lb ∧ l4 = lb@a::l2.
+#A #l1 #l2 #l3 generalize in match l1; generalize in match l2; elim l3
+  [normalize #l1 #l2 #l4 #a #H #_ @(ex_intro … []) @(ex_intro … l2) /2/
+  |#b #tl #Hind #l1 #l2 #l4 #a cases l2 
+    [normalize #Heq destruct >(\b (refl … b)) normalize #Hfalse destruct
+    |#c #tl2 whd in ⊢ ((??%%)→?); #Heq destruct #Hmema 
+     cases (Hind l1 tl2 l4 a ??)
+      [#l5 * #l6 * #eql #eql4 
+       @(ex_intro … (b::l5)) @(ex_intro … l6) % /2/
+      |@e0
+      |cases (true_or_false (memb ? a tl)) [2://]
+       #H @False_ind @(absurd ?? not_eq_true_false)
+       <Hmema @sym_eq @memb_cons //
+      ]
+    ]
+  ]
+qed. 
+         
 (*axiom list_decompose_memb :
   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → memb A a l3 = true.*)
 
@@ -273,4 +291,3 @@ elim Htable
    >associative_append % ]
 ]
 qed.
-