Quelle AdvancedCanonicalStructure.v Sprache: Coq

Require Import TestSuite.admit.
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.
  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.

Variable foo : A -> Type.

Definition local0 := fun (a1 : A) (a2 : A) (a3 : A) =>
                       (eq_refl : plusA a1 (plusA zeroA a2) = ia _).
Definition local1 :=
  fun (a1 : A) (a2 : A) (f : A -> A) =>
    (eq_refl : plusA a1 (plusA zeroA (f a2)) = ia _).

Definition local2 :=
  fun (a1 : A) (f : A -> A) =>
    (eq_refl : (f a1) = ia _).

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.
intros a b.
change (a * b = interp a * interp b).
rewrite (link a), (link b); reflexivity.
Qed.

Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
Proof.
intros a b.
change ((a -> b) = (interp a -> interp b)).
rewrite (link a), (link b); reflexivity.
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.

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.