|
(* Interaction between coercions and casts *)
(* Example provided by Eduardo Gimenez *)
Parameter Z S : Set.
Parameter f : S -> Z.
Coercion f : S >-> Z.
Parameter g : Z -> Z.
Check (fun s => g (s:S)).
(* Check uniform inheritance condition *)
Parameter h : nat -> nat -> Prop.
Parameter i : forall n m : nat, h n m -> nat.
Coercion i : h >-> nat.
(* Check coercion to funclass when the source occurs in the target *)
Parameter C : nat -> nat -> nat.
Coercion C : nat >-> Funclass.
(* Remark: in the following example, it cannot be decided whether C is
from nat to Funclass or from A to nat. An explicit Coercion command is
expected
Parameter A : nat -> Prop.
Parameter C:> forall n:nat, A n -> nat.
*)
(* Check coercion between products based on eta-expansion *)
(* (there was a de Bruijn bug until rev 9254) *)
Section P.
Variable E : Set.
Variables C D : E -> Prop.
Variable G :> forall x, C x -> D x.
Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y).
End P.
(* Check that class arguments are computed the same when looking for a
coercion and when applying it (class_args_of) (failed until rev 9255) *)
Section Q.
Variable bool : Set.
Variables C D : bool -> Prop.
Variable G :> forall x, C x -> D x.
Variable f : nat -> bool.
Definition For_all (P : nat -> Prop) := forall x, P x.
Check fun (H : For_all (fun x => C (f x))) => H : forall x, D (f x).
Check fun (H : For_all (fun x => C (f x))) x => H x : D (f x).
Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
End Q.
(* Combining class lookup and path lookup so that if a lookup fails, another
descent in the class can be found (see wish #1934) *)
Record Setoid : Type :=
{ car :> Type }.
Record Morphism (X Y:Setoid) : Type :=
{evalMorphism :> X -> Y}.
Definition extSetoid (X Y:Setoid) : Setoid.
constructor.
exact (Morphism X Y).
Defined.
Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
(* Check that coercions are made visible only when modules are imported *)
Module A.
Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B.
Fail Check S true.
End A.
Import A.
Fail Check S true.
(* Tests after the inheritance condition constraint is relaxed *)
Inductive list (A : Type) : Type :=
nil : list A | cons : A -> list A -> list A.
Inductive vect (A : Type) : nat -> Type :=
vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n).
Fixpoint size A (l : list A) : nat := match l with nil _ => 0 | cons _ _ tl => 1+size _ tl end.
Section test_non_unif_but_complete.
Fixpoint l2v A (l : list A) : vect A (size A l) :=
match l as l return vect A (size A l) with
| nil _ => vnil A
| cons _ x xs => vcons A (size A xs) x (l2v A xs)
end.
Local Coercion l2v : list >-> vect.
Check (fun l : list nat => (l : vect _ _)).
End test_non_unif_but_complete.
Section what_we_could_do.
Variables T1 T2 : Type.
Variable c12 : T1 -> T2.
Class coercion (A B : Type) : Type := cast : A -> B.
Instance atom : coercion T1 T2 := c12.
Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) :=
fun x => (c1 (fst x), c2 (snd x)).
Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) :=
match l as l return vect B (size A l) with
| nil _ => vnil B
| cons _ x xs => vcons _ _ (c x) (l2v2 xs) end.
Local Coercion l2v2 : list >-> vect.
(* This shows that there is still something to do to take full profit
of coercions *)
Fail Check (fun l : list (T1 * T1) => (l : vect _ _)).
Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)).
End what_we_could_do.
(** Unit test for Prop as source class *)
Module TestPropAsSourceCoercion.
Parameter heap : Prop.
Parameter heap_empty : heap.
Definition hprop := heap -> Prop.
Coercion hpure (P:Prop) : hprop := fun h => h = heap_empty /\ P.
Parameter heap_single : nat -> nat -> hprop.
Parameter hstar : hprop -> hprop -> hprop.
Notation "H1 \* H2" := (hstar H1 H2) (at level 69).
Definition test := heap_single 4 5 \* (5 <> 4) \* heap_single 2 4 \* (True).
(* Print test. -- reveals [hpure] coercions *)
End TestPropAsSourceCoercion.
(** Unit test for Type as source class *)
Module TestTypeAsSourceCoercion.
Require Import Coq.Setoids.Setoid.
Record setoid := { A : Type ; R : relation A ; eqv : Equivalence R }.
Definition default_setoid (T : Type) : setoid
:= {| A := T ; R := eq ; eqv := _ |}.
Coercion default_setoid : Sortclass >-> setoid.
Definition foo := Type : setoid.
Inductive type := U | Nat.
Inductive term : type -> Type :=
| ty (_ : Type) : term U
| nv (_ : nat) : term Nat.
Coercion ty : Sortclass >-> term.
Definition ty1 := Type : term _.
Definition ty2 := Prop : term _.
Definition ty3 := Set : term _.
Definition ty4 := (Type : Type) : term _.
End TestTypeAsSourceCoercion.
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
