after a PITA, lebergue is dualized!

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_copy.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/q_copy.ma b/helm/software/matita/contribs/dama/dama/models/q_copy.ma
index 00788cd16d0693319bf6dc2c438de4feea383194..de7384077ee93d07a1dfcbbdb12974b29a388dab 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_copy.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_copy.ma
@@ -93,13 +93,50 @@ lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros
 [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
 qed.
 
+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+    simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+    simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K); 
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+    unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+    simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+    cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.
 
+lemma value_tail : 
+  ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) (a::b::l) ▭);
+[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros;
+    [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6]
+        apply (q_lt_corefl ? (q_lt_le_trans ??? H H3));
+    |2:         
+
+normalize in ⊢ (? ? % ?→?); simplify;
+[1: rewrite > (value_head);
+ 
 lemma value_copy : 
-  ∀l,h1,h2,i,h3.
-  value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉.
-intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);]
-cases l1 in H H1 H2 H3;
-[1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?); 
+  ∀l,i.rewrite > (value_u
+  value_simple (copy l) i = 〈OQ,OQ〉.
+intros; elim l;
+[1: reflexivity;
+|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?);
+    [1: rewrite > (value_unit); reflexivity;
+    |2: cases (q_cmp (\fst b) (Qpos i));  
+ 
+ change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain; 
+    cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭);
+    [1: simplify in H1:(??%%);
+
+ unfold match_pred;
     rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
 |2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
     cases (q_cmp (Qpos i)  (\fst b));