From 39a701aa3ab9a3dcbeaa1dff4fcf43ea666e7f61 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 10:25:15 +0000 Subject: [PATCH] New bug exposed. --- helm/matita/tests/elim.ma | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index fcc130e9e..7c4031971 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -53,3 +53,27 @@ qed. theorem foo: let ax \def refl_equal ? 0 in t ax = t ax. elim t; reflexivity. qed. + +(* This test shows a bug where elim opens a new unus{ed,eful} goal *) + +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". + +inductive sum (n:nat) : nat \to nat \to Set \def + k: \forall x,y. n = x + y \to sum n x y. + +theorem t: \forall x,y. \forall H: sum x y O. + match H with [ (k a b p) \Rightarrow a ] = x. + intros. + cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x). + apply Hcut; reflexivity. + apply + (sum_ind ? + (\lambda a,b,K. y=a \to O=b \to + match K with [ (k a b p) \Rightarrow a ] = x) + ? ? ? H). + simplify. intros. + generalize in match H1. + rewrite < H2; rewrite < H3.intro. + rewrite > H4.auto. +qed. -- 2.39.2