From 35ead7a5cc04184e60688e7cb38549e7772577c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Jul 2007 10:41:15 +0000 Subject: [PATCH] more stuff about coercions --- matita/tests/coercions_dupelim.ma | 31 ++++++++++++++++++ matita/tests/coercions_nonuniform.ma | 49 ++++++++++++++++++++++++++++ 2 files changed, 80 insertions(+) create mode 100644 matita/tests/coercions_dupelim.ma create mode 100644 matita/tests/coercions_nonuniform.ma diff --git a/matita/tests/coercions_dupelim.ma b/matita/tests/coercions_dupelim.ma new file mode 100644 index 000000000..bfe2b3438 --- /dev/null +++ b/matita/tests/coercions_dupelim.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/". + +include "nat/nat.ma". + +axiom A : Type. + +inductive vec : nat -> Type := + | vnil : vec O + | vcons : ∀x:A.∀n:nat. vec n -> vec (S n). + +definition f := λx,n.λv:vec n.vcons x n v. +definition g := λn,x.λv:vec n.vcons x n v. + +include "logic/equality.ma". + +(* definition xx := f = g. *) +theorem xx1 : ∀n.∀x1:vec n.f ? ? x1 = g ? ? x1. diff --git a/matita/tests/coercions_nonuniform.ma b/matita/tests/coercions_nonuniform.ma new file mode 100644 index 000000000..bed1d73dc --- /dev/null +++ b/matita/tests/coercions_nonuniform.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/". + +axiom A : Type. +axiom B : A -> Type. +axiom f : A -> A. +axiom f1 : A -> A. + +axiom c : ∀a:A.B (f a). + +coercion cic:/matita/test/c.con. + +axiom C : Type. + +(* axiom c1 : ∀a:A. B (f a) -> C. *) (* COQ NO: non uniform *) +(* axiom c1 : ∀a:A. B (f1 a) -> C. *) (* non si compongono, ma almeno ho le 2 non composte le ho e le posso usare *) +(* axiom c1 : ∀f.∀a:A.B (f a) -> C. *) (* COQ NO: non uniform *) + +(* COQ NO: non uniform *) +axiom c2 : ∀a.B (f a) -> B (f1 a). +axiom c1 : ∀a:A. B (f1 a) -> C. + +coercion cic:/matita/test/c1.con. +coercion cic:/matita/test/c2.con. + +axiom g : C -> C. + +definition test := λa:A.g a. + +(* +Coq < Coercion c1 : B >-> C. +User error: c1 does not respect the inheritance uniform condition +*) + + + -- 2.39.2