From 35525e5acd7854210e2a1bbba07a4909117029ac Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 8 Sep 2007 17:21:58 +0000
Subject: [PATCH] Full specification of find. Added notation for If_Then_Else.
 Probably a delta on t in the match the decides if it is the case to pass a
 coercion under a match whould be nice.

---
 matita/tests/coercions_russell.ma | 110 +++++++++++++++---------------
 1 file changed, 56 insertions(+), 54 deletions(-)

diff --git a/matita/tests/coercions_russell.ma b/matita/tests/coercions_russell.ma
index f504cef72..dede79ca1 100644
--- a/matita/tests/coercions_russell.ma
+++ b/matita/tests/coercions_russell.ma
@@ -82,61 +82,63 @@ definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro
 
 coercion cic:/matita/test/russell/eject_opt.con.
 
-definition find :
- ∀p:nat → bool.
-  ∀l:list nat. sigma ? (λres:option nat.
+(* we may define mem as in the following lemma and get rid of it *)
+definition find_spec ≝
+  λl,p.λres:option nat.
    match res with
     [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
-    | Some x ⇒ mem ? eqb x l = true ∧ p x = true ]).
-letin program ≝
- (λp.
+    | Some x ⇒ mem ? eqb x l = true ∧ 
+               p x = true ∧ 
+               ∀y.mem ? eqb y l = true → p y = true → x ≠ y → 
+                    ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3].
+
+lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2.
+intros 2; elim l (H hd tl IH H); [destruct H]
+generalize in match H; clear H;
+simplify; apply (eqb_elim x hd); simplify; intros;
+[1:clear IH; rewrite < H; apply (ex_intro ? ? []); 
+|2:lapply(IH H1); clear H1 IH; decompose; rewrite > H2; clear H2]
+simplify; autobatch;
+qed.
+
+definition if : ∀A:Type.bool → A → A → A ≝ 
+ λA,b,t,f. match b with [ true ⇒ t | false ⇒ f].
+ 
+notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }.
+notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }.
+interpretation "if" 'if a b c = (cic:/matita/test/russell/if.con _ a b c). 
+
+definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
+(* define the find function *) 
+letin find ≝ (λp. 
   let rec aux l ≝
-   match l with
+    match l with
     [ nil ⇒ raise_exn
-    | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ]
-    ]
-  in
-   aux);
-apply
- (program : ∀p:nat → bool.
-  ∀l:list nat. ∃res:option nat.
-   match res with
-    [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false
-    | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]);
-clear program;
- [ cases (aux l1); clear aux;
-   simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]);
-   generalize in match H2; clear H2;
-   cases a;
-    [ simplify;
-      intros 2;
-      apply (eqb_elim y n);
-       [ intros;
-         autobatch
-       | intros;
-         apply H2;
-         simplify in H4;
-         exact H4
-       ]
-    | simplify;
-      intros;
-      cases H2; clear H2;
-      split;
-       [ elim (eqb n1 n);
-         simplify;
-         autobatch
-       | assumption
-       ]
-    ]
- | unfold nat_return; simplify;
-   split;
-    [ rewrite > eqb_n_n;
-      reflexivity
-    | assumption
-    ]
- | unfold raise_exn; simplify;
-   intros;
-   change in H1 with (false = true);
-   destruct H1 
- ]
-qed.
\ No newline at end of file
+    | cons x l ⇒ If p x Then nat_return x Else aux l]
+    in aux);
+(* manca una delta?! *) unfold if in find;
+apply (find: ∀p.∀l.sigma ? (λres.find_spec l p res)); clear find;
+(* 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;
+    |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 ⊢ (? ? ? %→?); 
+            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;
+                simplify; autobatch depth = 4;]]]
+(* l = x::tl ∧ p x = true *)
+|2: unfold find_spec; unfold nat_return; simplify; repeat split; [2: assumption]
+    [1: rewrite > eqb_n_n; reflexivity
+    |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;]]
+(* l = [] *)
+|3: unfold raise_exn; simplify; intros; destruct H1;]
+qed.
-- 
2.39.2