From: Claudio Sacerdoti Coen Date: Wed, 5 Sep 2007 10:35:46 +0000 (+0000) Subject: added fix case X-Git-Tag: 0.4.95@7852~225 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=033ef07477e15b36c2865f91c0ccf139a66e6fd7;p=helm.git added fix case --- diff --git a/matita/tests/coercions_propagation.ma b/matita/tests/coercions_propagation.ma index c8529631b..af5f2435c 100644 --- a/matita/tests/coercions_propagation.ma +++ b/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