From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Apr 2009 12:59:20 +0000 (+0000)
Subject: Some improvements.
X-Git-Tag: make_still_working~4069
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6bd0d331d096d862754b42f9a7fb8af1b823685d;p=helm.git

Some improvements.
---

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index 448217888..48639b3cb 100644
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/matita/tests/coercions_russell.ma
@@ -34,23 +34,16 @@ coercion cic:/matita/tests/coercions_russell/eject.con.
   
 alias symbol "exists" (instance 2) = "exists".
 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
-letin program ≝ 
-  (λl:list nat. λH:l ≠ [].match l with [ nil ⇒ λH.[] | cons x l1 ⇒ λH.l1] H);
-letin program_spec ≝ (program : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l);
- [ generalize in match H; cases l; [intros (h1); cases (h1 ?); reflexivity]
-   intros; apply (ex_intro ? ? n); apply eq_f; reflexivity; ]
-exact program_spec;
+ apply rule (λl:list nat. λ_.match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
+  [ exists; [2: reflexivity | skip]
+  | destruct; elim H; reflexivity]
 qed.
 
 alias symbol "exists" (instance 3) = "exists".
 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
-apply
-  (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]
-  :
-  ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
+apply rule (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
 [ autobatch; 
-| generalize in match H; clear H; cases s; simplify;
-  intros; cases (H H1);]
+| cases s in H; simplify; intros; cases (H H1); ]
 qed.
 
 definition nat_return := λn:nat. Some ? n.
@@ -104,24 +97,22 @@ qed.
 notation > "'If' b 'Then' t 'Else' f" non associative
 with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
 
-definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
-(* define the find function *) 
-apply (λp. 
+alias symbol "exists" = "sigma".
+definition sigma_find_spec : ∀p,l. ∃res.find_spec l p res.
+apply rule (λp. 
   let rec aux l ≝
     match l with
     [ nil ⇒ raise_exn
     | cons x l ⇒ If p x Then nat_return x Else aux l]
-    in aux
-  : 
-  ∀p.∀l.sigma ? (λres.find_spec l p res));
+    in aux);
 (* l = x::tl ∧ p x = false *)
 [1: cases (aux l1); clear aux;
-    generalize in match H2; clear H2; cases a; clear a; simplify;
-    [1: intros 2; apply (eqb_elim y n); intros (Eyn); [rewrite > Eyn; assumption]
-        apply H3; simplify in H2; assumption;
+    cases a in H2; simplify;
+    [1: intros 2; apply (eqb_elim y n); intros (Eyn); autobatch;
     |2: intros; decompose; repeat split; [2: assumption]; intros;
         [1: cases (eqb n1 n); simplify; autobatch;
-        |2: generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?); 
+        |2: generalize in match (refl_eq ? (eqb y n));
+            generalize in ⊢ (? ? ? %→?); 
             intro; cases b; clear b; intro Eyn; rewrite > Eyn in H3; simplify in H3;
             [1: rewrite > (eqb_true_to_eq ? ? Eyn) in H6; rewrite > H1 in H6; destruct H6;
             |2: lapply H4; try assumption; decompose; clear H4; rewrite > H8;
@@ -132,9 +123,9 @@ apply (λp.
     |2: intro; generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
         intro; cases b; clear b; intro Eyn; rewrite > Eyn; 
         [1: rewrite > (eqb_true_to_eq ? ? Eyn);] clear Eyn; simplify; intros;
-        [1: cases H4; reflexivity
-        |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
-            apply (ex_intro ? ? []); simplify; autobatch;]]
+          [1: cases H4; reflexivity
+          |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
+              apply (ex_intro ? ? []); simplify; autobatch;]]
 (* l = [] *)
 |3: unfold raise_exn; simplify; intros; destruct H1;]
-qed.
+qed.
\ No newline at end of file