Quelle fixpointeta.v Sprache: Coq

Set Primitive Projections.

Record R := C { p : nat }.
(* R is defined
p is defined *)

Unset Primitive Projections.
Record R' := C' { p' : nat }.

Fail Definition f := fix f (x : R) : nat := p x.
(** Not allowed to make fixpoint defs on (non-recursive) records
  having eta *)

Fail Definition f := fix f (x : R') : nat := p' x.
(** Even without eta (R' is not primitive here), as long as they're
  found to be BiFinite (non-recursive), we disallow it *)

(*

(* Subject reduction failure example, if we allowed fixpoints *)

Set Primitive Projections.

Record R := C { p : nat }.

Definition f := fix f (x : R) : nat := p x.

(* eta rule for R *)
Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x
:= v.

Definition goal := forall x, f x = p x.

(* when we compute the Rtr away typechecking will fail *)
Definition thing : goal := fun x =>
(Rtr (fun x => f x = p x) x (eq_refl _)).

Definition thing' := Eval compute in thing.

Fail Check (thing = thing').
(*
The command has indeed failed with message:
The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)"
and "f x = p x").
*)

Definition thing_refl := eq_refl thing.

Fail Definition thing_refl' := Eval compute in thing_refl.
(*
The command has indeed failed with message:
Illegal application:
The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
cannot be applied to the terms
"forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop"
"fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
which should be coercible to
"forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)".
*)

Definition more_refls : thing_refl = thing_refl.
Proof.
  compute. reflexivity.
Fail Defined. Abort.
*)

quality99%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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.