Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / tests / coercions_russell.ma

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index dede79ca145e741115813aac4ebff05b48cedb13..203faece5d6db7e13ef284842fe397502e6a0bb3 100644 (file)
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/matita/tests/coercions_russell.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/russell/".
+
 
 include "nat/orders.ma".
 include "list/list.ma".
@@ -22,15 +22,15 @@ inductive sigma (A:Type) (P:A → Prop) : Type ≝
  sig_intro: ∀a:A. P a → sigma A P.
 
 interpretation "sigma" 'exists \eta.x =
-  (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x).
+  (cic:/matita/tests/coercions_russell/sigma.ind#xpointer(1/1) _ x).
  
 definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
 
-coercion cic:/matita/test/russell/inject.con 0 1.
+coercion cic:/matita/tests/coercions_russell/inject.con 0 1.
 
 definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
 
-coercion cic:/matita/test/russell/eject.con.
+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.
@@ -55,7 +55,7 @@ qed.
 
 definition nat_return := λn:nat. Some ? n.
 
-coercion cic:/matita/test/russell/nat_return.con.
+coercion cic:/matita/tests/coercions_russell/nat_return.con.
 
 definition raise_exn := None nat.
 
@@ -76,11 +76,11 @@ 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.
+coercion cic:/matita/tests/coercions_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.
+coercion cic:/matita/tests/coercions_russell/eject_opt.con.
 
 (* we may define mem as in the following lemma and get rid of it *)
 definition find_spec ≝
@@ -93,7 +93,7 @@ definition find_spec ≝
                     ∃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]
+intros 2; elim l (H hd tl IH H); [simplify in 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 ? ? []); 
@@ -106,7 +106,7 @@ definition if : ∀A:Type.bool → A → A → A ≝
  
 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). 
+interpretation "if" 'if a b c = (cic:/matita/tests/coercions_russell/if.con _ a b c). 
 
 definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
 (* define the find function *)