diff options
author | 2008-02-14 13:59:33 +0000 | |
---|---|---|
committer | 2008-02-14 13:59:33 +0000 | |
commit | 921f0ef22fcd79e69486e0aec75e57f68dce661e (patch) | |
tree | a8a62246fdbb6363e1f3e1a39d5b8d5ca1c27fcd /test-suite | |
parent | bb3560885d943baef87b7f99a5d646942f0fb288 (diff) |
Added default canonical structures (see example in test-suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/DefaultCanonicalStructure.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/test-suite/success/DefaultCanonicalStructure.v b/test-suite/success/DefaultCanonicalStructure.v new file mode 100644 index 000000000..f21ea7c8a --- /dev/null +++ b/test-suite/success/DefaultCanonicalStructure.v @@ -0,0 +1,49 @@ + +(* An example with default canonical structures *) + +Variable A B : Type. +Variable plusA : A -> A -> A. +Variable plusB : B -> B -> B. +Variable zeroA : A. +Variable zeroB : B. +Variable eqA : A -> A -> Prop. +Variable eqB : B -> B -> Prop. +Variable phi : A -> B. + +Set Implicit Arguments. + +Record img := { + ia : A; + ib :> B; + prf : phi ia = ib +}. + +Parameter eq_img : forall (i1:img) (i2:img), + eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2). + +Lemma phi_img (a:A) : img. + intro a. + exists a (phi a). + refine ( refl_equal _). +Defined. +Canonical Structure phi_img. + +Lemma zero_img : img. + exists zeroA zeroB. + admit. +Defined. +Canonical Structure zero_img. + +Lemma plus_img : img -> img -> img. +intros i1 i2. +exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)). +admit. +Defined. +Canonical Structure plus_img. + +Print Canonical Projections. + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _); simpl. +Admitted. |