From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 Sep 2007 10:35:46 +0000 (+0000)
Subject: added fix case
X-Git-Tag: make_still_working~6074
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9376f52b7f5890d924ae7d93bcae2af9e516126d;p=helm.git

added fix case
---

diff --git a/helm/software/matita/tests/coercions_propagation.ma b/helm/software/matita/tests/coercions_propagation.ma
index c8529631b..af5f2435c 100644
--- a/helm/software/matita/tests/coercions_propagation.ma
+++ b/helm/software/matita/tests/coercions_propagation.ma
@@ -54,6 +54,99 @@ theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
  assumption.
 qed.
 
+(* guarded troppo debole 
+theorem test5: nat → ∃n. 1 ≤ n.
+apply (
+ let rec aux n : nat ≝
+  match n with
+   [ O ⇒ 1
+   | S m ⇒ S (aux m)
+   ]
+ in
+  aux
+: nat → ∃n. 1 ≤ n);
+cases name_con;
+simplify;
+ [ autobatch
+ | cases (aux n);
+   simplify;
+   apply lt_O_S
+ ]
+qed.
+*)
+
+(*
+theorem test5: nat → ∃n. 1 ≤ n.
+apply (
+ let rec aux (n : nat) : ∃n. 1 ≤ n ≝ 
+   match n with
+   [ O => (S O : ∃n. 1 ≤ n)
+   | S m => (S (aux m) : ∃n. 1 ≤ n)
+(*      
+   inject ? (S (eject ? (aux m))) ? *)
+   ]
+ in
+  aux
+ : nat → ∃n. 1 ≤ n);
+ [ autobatch
+ | elim (aux m);
+   simplify;
+   autobatch
+ ]
+qed.
+
+Re1: nat => nat |- body[Rel1] : nat => nat
+Re1: nat => X |- body[Rel1] : nat => nat : nat => X
+Re1: Y => X |- body[Rel1] : nat => nat : Y => X
+
+nat => nat
+nat => X
+
+theorem test5: (∃n. 2 ≤ n) → ∃n. 1 ≤ n.
+apply (
+ λk: ∃n. 2 ≤ n.
+ let rec aux n : eject ? n = eject ? k → ∃n. 1 ≤ n ≝
+  match eject ? n return λx:nat. x = eject ? k → ∃n. 1 ≤ n with
+   [ O ⇒ λH: 0 = eject ? k.
+          sigma_intro ? ? 0 ?
+   | S m ⇒ λH: S m = eject ? k.
+          sigma_intro ? ? (S m) ?
+   ]
+ in
+  aux k (refl_eq ? (eject ? k)));
+
+
+intro;
+cases s; clear s;
+generalize in match H; clear H;
+elim a;
+ [ apply (sigma_intro ? ? 0);
+ | apply (sigma_intro ? ? (S n));
+ ].
+
+apply (
+ λk.
+ let rec aux n : ∃n. 1 ≤ n ≝
+  inject ?
+   (match n with
+     [ O ⇒ O
+     | S m ⇒ S (eject ? (aux m))
+     ]) ?
+ in aux (eject ? k)).
+
+   
+apply (
+ let rec aux n : nat ≝
+  match n with
+   [ O ⇒ O
+   | S m ⇒ S (aux m)
+   ]
+ in
+  aux
+: (∃n. 2 ≤ n) → ∃n. 1 ≤ n);
+
+qed.
+
 (*
 theorem test5: nat → ∃n. 0 ≤ n.
  apply (λn:nat.?);
@@ -63,3 +156,4 @@ theorem test5: nat → ∃n. 0 ≤ n.
  autobatch.
 qed.
 *)
+*)
\ No newline at end of file