X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fcoercions_russell.ma;h=f504cef72e9e2a97576892e4d9d003c28df95722;hb=00bb9e0e9e23b6d68e0d56bdeb96245673495a68;hp=50bf81dfd44647c6970923381b708c168175d3ef;hpb=aa654b256f9deca4ed5bb2b13b87e1d69377f17d;p=helm.git

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index 50bf81dfd..f504cef72 100644
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/matita/tests/coercions_russell.ma
@@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/test/russell/".
 
 include "nat/orders.ma".
 include "list/list.ma".
+include "datatypes/constructors.ma".
 
 inductive sigma (A:Type) (P:A → Prop) : Type ≝
  sig_intro: ∀a:A. P a → sigma A P.
@@ -51,3 +52,91 @@ letin program_spec ≝
     intros; cases (H H1); ]
 exact program_spec.
 qed.
+
+definition nat_return := λn:nat. Some ? n.
+
+coercion cic:/matita/test/russell/nat_return.con.
+
+definition raise_exn := None nat.
+
+definition try_with :=
+ λx,e. match x with [ None => e | Some (x : nat) => x].
+
+lemma hd : list nat → option nat :=
+  λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
+  
+axiom f : nat -> nat.
+
+definition bind ≝ λf:nat->nat.λx.
+  match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
+
+include "datatypes/bool.ma".
+include "list/sort.ma".
+include "nat/compare.ma".
+
+definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
+
+coercion cic:/matita/test/russell/inject_opt.con 0 1.
+
+definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
+
+coercion cic:/matita/test/russell/eject_opt.con.
+
+definition find :
+ ∀p:nat → bool.
+  ∀l:list nat. sigma ? (λ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.
+  let rec aux l ≝
+   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