From b87b8d16e74b1f6072e87f02c1cec78521e6791c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Apr 2008 15:42:10 +0000 Subject: [PATCH] added ugly test showing many many bugs in the current kernel --- .../tests/dependent_guarded_bove_capretta.ma | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 helm/software/matita/tests/dependent_guarded_bove_capretta.ma diff --git a/helm/software/matita/tests/dependent_guarded_bove_capretta.ma b/helm/software/matita/tests/dependent_guarded_bove_capretta.ma new file mode 100644 index 000000000..b9cdfa50e --- /dev/null +++ b/helm/software/matita/tests/dependent_guarded_bove_capretta.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/nat.ma". + +inductive T : Prop := + | l : T + | r : T-> T. + +inductive Q : nat -> T -> Prop := + | lq : Q O l + | lr : ∀n,t.Q (S (S n)) t -> Q n (r t). + +axiom F : False. + +definition xxx := λt.(match t return (λt:T.T) with + [ l => match F in False with [] + | r (t1:T) => t1]). + +let rec f (n:nat) (t:T) on t :nat := + (match n with + [ O => O + | S mmm => + f (S (S mmm)) (xxx t)]). + +let rec f (n:nat) (t:T) on t : Q n t -> nat := + (match n with + [ O => λ_.O + | S mmm => λq:Q (S mmm) (r t). + f (S (S mmm)) + (match t return (λt:T.T) with + [ l => match F in False with [] + | r (t1:T) => t1]) + + (match q return λn,t,x.Q (S (S n)) t with + [ lq => match F in False return λ_.Q (S (S n)) t with [] + | lr k t qsskt => qsskt]) + ]). + -- 2.39.2