1 files changed, 144 insertions, 0 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
new file mode 100644
index 00000000..8e613dca
--- /dev/null
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -0,0 +1,144 @@
+Section group_morphism.
+
+(* 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.
+
+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 _ _  _).
+change (eqB (plusB (phi a1) zeroB) (phi a2)).
+Admitted.
+
+End group_morphism.
+
+Open Scope type_scope.
+
+Section type_reification.
+
+Inductive term :Type := 
+   Fun : term -> term -> term
+ | Prod : term -> term -> term
+ | Bool : term
+ | SET :term
+ | PROP :term
+ | TYPE :term
+ | Var : Type -> term.
+
+Fixpoint interp (t:term) := 
+  match t with 
+    Bool => bool
+  | SET => Set
+  | PROP => Prop
+  | TYPE => Type   
+  | Fun a b => interp a -> interp b
+  | Prod a b => interp a * interp b
+  | Var x => x
+end.
+
+Record interp_pair :Type := 
+  { repr:>term;
+    abs:>Type;
+    link: abs = interp repr }.
+
+Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
+proof.
+let a:interp_pair,b:interp_pair.
+reconsider thesis as (a * b = interp a * interp b).
+thus thesis by (link a),(link b).
+end proof.
+Qed.
+
+Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
+proof.
+let a:interp_pair,b:interp_pair.
+reconsider thesis as ((a -> b) = (interp a -> interp b)).
+thus thesis using rewrite (link a);rewrite (link b);reflexivity.
+end proof.
+Qed.
+
+Canonical Structure ProdCan (a b:interp_pair) := 
+  Build_interp_pair (Prod a b) (a * b) (prod_interp a b).
+
+Canonical Structure FunCan (a b:interp_pair) := 
+  Build_interp_pair (Fun a b) (a -> b) (fun_interp a b).
+
+Canonical Structure BoolCan := 
+  Build_interp_pair Bool bool (refl_equal _).
+
+Canonical Structure VarCan (x:Type) := 
+  Build_interp_pair (Var x) x (refl_equal _).
+
+Canonical Structure SetCan := 
+  Build_interp_pair SET Set (refl_equal _).
+
+Canonical Structure PropCan := 
+  Build_interp_pair PROP Prop (refl_equal _).
+
+Canonical Structure TypeCan := 
+  Build_interp_pair TYPE Type (refl_equal _).
+
+(* Print Canonical Projections. *)
+
+Variable A:Type.
+
+Variable Inhabited: term -> Prop.
+
+Variable Inhabited_correct: forall p, Inhabited (repr p)  -> abs p.
+
+Lemma L : Prop * A -> bool * (Type -> Set) .
+refine (Inhabited_correct _ _).
+change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
+Admitted.
+
+Check L : abs _ .
+
+End type_reification.
+
+
+
+
+
+
+
+
+ 
+