From 3e77313de19d2343092148e8a94161b2a8996a4d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 15 Oct 2007 11:29:04 +0000 Subject: [PATCH] Spurious code removed. Destruct fails recursively. --- matita/tests/discriminate.ma | 32 +++----------------------------- 1 file changed, 3 insertions(+), 29 deletions(-) diff --git a/matita/tests/discriminate.ma b/matita/tests/discriminate.ma index b1d7b9ca6..1d6a51494 100644 --- a/matita/tests/discriminate.ma +++ b/matita/tests/discriminate.ma @@ -86,37 +86,11 @@ qed. theorem recursive4: ∀ x,y,z,t : nat. C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) = C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t. -intros; - - - - - (λHH : ((C1 (option nat) nat (S O) (Some nat -7) -8) = (C1 (option nat) nat (S O) (Some nat -9) -8)) - eq_elim_r - (complex (option nat) nat -8 (Some nat -7)) - (C1 (option nat) nat (S O) (Some nat -9) -8) - (λc:(complex (option nat) nat -8 (Some nat -7)). - (eq (option nat) - ((λx:(complex (option nat) nat -8 (Some nat -7)). - match x return (λy1:nat.(λy2:(option nat).(λ x:(complex (option nat) nat y1 y2).(option nat)))) with - [ (C1 (y1:nat) (a:(option nat)) (b:nat)) => a - | (C2 (a:(option nat)) (a1:(option nat)) (b:nat) (b1:nat) (y2:nat) (y3:(complex (option nat) nat b1 a1))) ⇒ - (Some nat -7) - ]) c) - (Some nat -9))) - ? - (C1 (option nat) nat (S O) (Some nat -7) -8) - HH) - - - - -destruct H;assumption. +intros; destruct H;assumption. qed. theorem recursive2: ∀ x,y : nat. C2 ? ? (None ?) ? (S O) ? O (C1 ? ? O (Some ? x) y) = C2 ? ? (None ?) ? (S O) ? O (C1 ? ? (S O) (Some ? x) y) → False. -intros; destruct H; - - +intros; destruct H. +qed. \ No newline at end of file -- 2.39.2