Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_2117.v Sprache: Coq

Original von: Coq^©

(* Check pattern-unification on evars in apply unification *)

Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.

Axiom copy : forall tau:Type, tau -> tau -> Prop.
Axiom copyr : forall tau:Type, tau -> tau -> Prop.
Axiom copyf : forall tau:Type, tau -> tau -> Prop.
Axiom eq : forall tau:Type, tau -> tau -> Prop.
Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.

Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
->copy (tau->tau') t t'.

Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
copyr (tau->tau') t t'
->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).

Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
copyr (tau->tau') t t'
->(forall x y:tau, forall z1 z2:tau',
(copy tau x y)->
(subst tau tau' t x z1)->
(subst tau tau' t' y z2)->
copyf tau' z1 z2).

Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
( ((subst tau tau' t q t') /\ (eq tau' t' r))
->eq tau' (app tau tau' t q) r).

Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
->eq tau' r (app tau tau' t q).

Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
->subst tau tau' t q r.

Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
Ltac Subst := apply substcopy;intros;EtaLong.
Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.

Theorem church0: forall i:Type, exists X:(i->i)->i->i,
copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
intros.
esplit.
EtaLong.
eapply eqappd;split.
Subst.
apply copyf_atom.
Show Existentials.
apply H1.
Abort.

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.