Quelle definition_using.v Sprache: Coq

Axiom bogus : Type.

Section A.
Variable x : bogus.

#[using="All"]
Definition c1 : bool := true.

#[using="All"]
Fixpoint c2 n : bool :=
  match n with
  | O => true
  | S p => c3 p
  end
with c3 n : bool :=
  match n with
  | O => true
  | S p => c2 p
end.

#[using="All"]
Definition c4 : bool. Proof. exact true. Qed.

#[using="All"]
Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed.

#[using="All"]
Definition c6 : bool. Proof. exact true. Qed.

#[using="All"]
Fixpoint c7 (n : nat) {struct n} : bool :=
  match n with
  | O => true
  | S p => c7 p
  end.

Fail #[using="dummy", program]
Fixpoint c7' (n : nat) {struct n} : bool :=
  match n with
  | O => true
  | S p => c7' p
  end.

Fail #[using="c7'", program]
Fixpoint c7' (n : nat) {struct n} : bool :=
  match n with
  | O => true
  | S p => c7' p
  end.

End A.

Check c1 : bogus -> bool.
Check c2 : bogus -> nat -> bool.
Check c3 : bogus -> nat -> bool.
Check c4 : bogus -> bool.
Check c5 : bogus -> nat -> bool.
Check c6 : bogus -> bool.
Check c7 : bogus -> nat -> bool.

Section B.

Variable a : bogus.
Variable h : c1 a = true.

#[using="a*"]
Definition c8 : bogus := a.

Collection ccc := a h.

#[using="ccc"]
Definition c9 : bogus := a.

#[using="ccc - h"]
Definition c10 : bogus := a.

End B.

Check c8 : forall a, c1 a = true -> bogus.
Check c9 : forall a, c1 a = true -> bogus.
Check c10: bogus -> bogus.

Module TypeBehavior.

Section S.
Variables a : nat.
#[using="Type", warning="-non-recursive"]
Program Fixpoint b1 (n:nat) : nat := (fun _ => 0) a.
Program Fixpoint b2 (n:nat) : (fun X _ => X) nat a := 0.
Program Fixpoint b3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
Program Definition c1 : nat := (fun _ => 0) a.
Program Definition c2 : (fun X _ => X) nat a := 0.
Program Definition c3 : (fun X _ => X) nat a := (fun _ => 0) a.
Fixpoint d1 (n:nat) : nat := (fun _ => 0) a.
Fixpoint d2 (n:nat) : (fun X _ => X) nat a := 0.
Fixpoint d3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
Definition e1 : nat := (fun _ => 0) a.
Definition e2 : (fun X _ => X) nat a := 0.
Definition e3 : (fun X _ => X) nat a := (fun _ => 0) a.
End S.
(* Not clear what is most expected below... *)

(* Dependency in a with Program Fixpoint: the body is not reduced. *)
(* As of now, we don't seem to have such a case. *)
(* No dependency in a with Program Fixpoint, because both body and type are beta-reduced *)
Check b1 0 : nat.
Check b2 0 : nat.
Check b3 0 : nat.
(* With Program Definition, type is beta-reduced but not the body *)
Check c1 0 : nat.
Check c2 : nat.
Check c3 0 : nat.
(* With Definition/Fixpoint, neither body nor type are beta-reduced *)
Check d1 0 0 : nat.
Check d2 0 0 : nat.
Check d3 0 0 : nat.
Check e1 0 : nat.
Check e2 0 : nat.
Check e3 0 : nat.

End TypeBehavior.

quality98%

¤ Dauer der Verarbeitung: 0.13 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.