Quelle Fixpoint.v Sprache: Coq

(* Playing with (co-)fixpoints with local definitions *)

Inductive listn : nat -> Set :=
  niln : listn 0
| consn : forall n:nat, nat -> listn n -> listn (S n).

Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
   match n with O => p | _ =>
     match l with niln => p | consn q _ l => f (S q) l end
   end.

Eval compute in (f 2 (consn 0 0 niln)).

CoInductive Stream : nat -> Set :=
  Consn : forall n, nat -> Stream n -> Stream (S n).

CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
    match n return (let m:=pred n in forall l:Stream m, let p:=S n in Stream p)
    with
    | O => fun l:Stream 0 => Consn O 0 l
    | S n' =>
      fun l:Stream n' =>
      let l' :=
        match l in Stream q return Stream (pred q) with Consn _ _ l => l end
      in
      let a := match l with Consn _ a l => a end in
      Consn (S n') (S a) (g n' l')
   end l.

Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).

(* Check inference of simple types in presence of non ambiguous
   dependencies (needs revision 10125) *)

Section folding.

Inductive vector (A:Type) : nat -> Type :=
  | Vnil : vector A 0
  | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n).

Variables (B C : Set) (g : B -> C -> C) (c : C).

Fixpoint foldrn n bs :=
  match bs with
  | Vnil _ => c
  | Vcons _ b _ tl => g b (foldrn _ tl)
  end.

End folding.

(* Check definition by tactics *)

Inductive even : nat -> Type :=
  | even_O : even 0
  | even_S : forall n, odd n -> even (S n)
with odd : nat -> Type :=
    odd_S : forall n, even n -> odd (S n).

Fixpoint even_div2 n (H:even n) : nat :=
  match H with
  | even_O => 0
  | even_S n H => S (odd_div2 n H)
  end
with odd_div2 n H : nat.
destruct H.
apply even_div2 with n.
assumption.
Qed.

Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat.
destruct H.
exact 0.
apply odd_div2' with n.
assumption.
destruct H.
apply even_div2' with n.
assumption.
Qed.

CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B
with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B.

CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool
with ex2 (n:nat) (b:bool) : Stream2 nat bool.
apply Cons1.
exact n.
apply (ex2 n b).
apply Cons2.
exact b.
apply (ex1 (S n) (negb b)).
Defined.

Section visibility.

  Let Fixpoint imm (n:nat) : True := I.

  Let Fixpoint by_proof (n:nat) : True.
  Proof. exact I. Defined.

  Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool.
  Proof.
    - destruct n as [|n].
      + exact true.
      + exact (bar n).
    - destruct n as [|n].
      + exact false.
      + exact (foo n).
  Qed.

  Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool.
  Admitted.

End visibility.

Fail Check imm.
Fail Check by_proof.
Check bla. Check bli.

Module Import mod_local.
  Fixpoint imm_importable (n:nat) : True := I.

  Local Fixpoint imm_local (n:nat) : True := I.

  Fixpoint by_proof_importable (n:nat) : True.
  Proof. exact I. Defined.

  Local Fixpoint by_proof_local (n:nat) : True.
  Proof. exact I. Defined.
End mod_local.

Check imm_importable.
Fail Check imm_local.
Check mod_local.imm_local.
Check by_proof_importable.
Fail Check by_proof_local.
Check mod_local.by_proof_local.

(* Miscellaneous tests *)

Module IotaRedex.

Fixpoint minus (n m:nat) {struct n} : nat :=
  match (n, m) with
  | (O , _) => O
  | (S _ , O) => n
  | (S n', S m') => minus n' m'
  end.

End IotaRedex.

Module ReturningInductive.

Fail Fixpoint geneq s (x: list nat) {struct s} : Prop :=
  match x with
  | cons a t => geneq (S a) t /\ geneq (S a) t
  | _ => False
  end.

End ReturningInductive.

Module NestingAndUnfolding.

Fail Fixpoint f (x:nat) := id (fix g x : nat := f x) 0.

Fixpoint f x :=
  match x with
  | 0 => 0
  | S n => id (fix g x := f x) n
  end.

End NestingAndUnfolding.

Module NestingAndConstructedUnfolding.

Definition fold_left {A B : Type} (f : A -> B -> A) :=
fix fold_left (l : list B) (a0 : A) {struct l} : A :=
  match l with
  | nil => a0
  | cons b t => fold_left t (f a0 b)
  end.

Record t A : Type :=
    mk {
        elt: A
      }.

Arguments elt {A} t.

Inductive LForm : Type :=
| LIMPL : t LForm -> list (t LForm) -> LForm.

Fixpoint hcons  (m : unit) (f : LForm) :=
  match f with
  | LIMPL f l => fold_left (fun m f => hcons m f.(elt) ) (cons f l) m
  end.
End NestingAndConstructedUnfolding.

Module CofixRedex.

CoInductive Stream := {hd : nat; tl : Stream}.
Definition zeros := cofix zeros := {|hd := 0; tl := zeros|}.

Fixpoint f n :=
  match n with
  | 0 => 0
  | S n =>
    match zeros with
    | {|hd:=_|} => fun f => f n
    end f
  end.

End CofixRedex.

Module CofixRedexPrimProj.

Set Primitive Projections.
CoInductive Stream A := {hd : A; tl : Stream A}.
Arguments hd {A} s.

Fixpoint f n :=
  match n with
  | 0 => 0
  | S n => (cofix cst := {|hd := (fun f => f n); tl := cst|}).(hd) f
  end.

End CofixRedexPrimProj.

Module ArgumentsAcrossMatch.

(* large subterm passed across match *)
Fail Fixpoint f n p {struct n} :=
  match n with
  | 0 => fun _ => 0
  | S q => fun r => f q (f r 0)
  end n.

(* strict subterm passed across match *)
Fixpoint f n p {struct n} :=
  match n with
  | 0 => 0
  | S q =>
     match q with
     | 0 => fun _ => 0
     | S q' => fun r => f q (f r 0)
     end q
  end.

End ArgumentsAcrossMatch.

Module LetToExpand.

Fixpoint h n :=
  let f n := (fun x : h n -> True => True) (fun y : h n => I) in
  match n with
  | 0 => True
  | S n => f n
  end.

End LetToExpand.

Module RecursiveCallInsideCoFix.

CoInductive I := { field : I }.

Fail Fixpoint f (n:nat) :=
  (cofix g n := {| field := f n |}) 0.

End RecursiveCallInsideCoFix.

Module NestedRedexes.

Fixpoint f n :=
  match n with
  | 0 => 0
  | S n => id (fun x => id (fun _ => id (f x)) 0) n
  end.

End NestedRedexes.

Module NestedRedexesWithCofix.

CoInductive I := { field : nat -> nat }.

Fail Fixpoint f n :=
  ((cofix g h := {| field := h |}) f).(field) n.

Fixpoint f n :=
  match n with
  | 0 => 0
  | S p => ((cofix g h := {| field := h |}) f).(field) p
  end.

End NestedRedexesWithCofix.

Module NestedApplicationsWithVariables.

Section S.
Variable h : (nat -> nat) -> nat.
Fixpoint f n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) (h f)
  end.
End S.

End NestedApplicationsWithVariables.

Module NestedApplicationsWithParameters.

Parameter h : (nat -> nat) -> nat.
Fixpoint f n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) (h f)
  end.

End NestedApplicationsWithParameters.

Module NestedApplicationsWithLocalVariables.

Fixpoint f (h:(nat->nat)->nat) n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) (h (f h))
  end.

End NestedApplicationsWithLocalVariables.

Module NestedApplicationsWithProjections.

Set Primitive Projections.
Record R := { field : (nat -> nat) -> nat }.

Fixpoint f x n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) (x.(field) (f x))
  end.

End NestedApplicationsWithProjections.

Module NestedRedexesWithFix.

Fixpoint f n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k) f)
  end.

(* inner fix fully applied with a match subterm *)
Fixpoint f' n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k) f' p)
  end.

(* inner fix fully applied with an arbitrary term *)
Fixpoint f'' o n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k o) f'' o)
  end.

End NestedRedexesWithFix.

Module NestedRedexesWithMatch.

Fixpoint f o n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) (match o with tt => f o end)
  end.

Fixpoint f' o n :=
  match n with
  | 0 => 0
  | S p => (fun _ => 0) ((match o with tt => fun x => x o end) f')
  end.

End NestedRedexesWithMatch.

Module ErasableInertSubterm.

Fixpoint P (n:nat) :=
  (fun _ => True) (forall a : (forall p, P p), True).

End ErasableInertSubterm.

Module WithLetInLift.

Fixpoint f (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n => (let x := 0 in fun n => f n) n
  end.

End WithLetInLift.

Module WithLateCaseReduction.

Definition B := true.
Fixpoint f (n : nat) :=
  match n with
  | 0 => 0
  | S n => (if B as b return if b then nat -> nat else unit then fun n => f n else tt) n
  end.

End WithLateCaseReduction.

Module NtnInteractiveFixpoint.

Reserved Notation "# n" (at level 2, right associativity).
Fixpoint f (n:nat) : nat where "# n" := (f n).
exact (match n with 0 => 0 | S n => # n end).
Defined.
Check eq_refl : # 0 = f 0.

End NtnInteractiveFixpoint.

Module NoArgumentFixpoint.

Fail Fixpoint f : nat. (* was an anomaly at some time *)

End NoArgumentFixpoint.

Module FixpointRelevance.

(* Check that the recursive reference to a fixpoint name has correct
   relevance, in different execution paths *)

Inductive STrue : SProp := SI.
Inductive seq (a:STrue) : STrue -> SProp := srefl : seq a a.
Fixpoint g1 (n:nat) : STrue :=
  match n with
  | 0 => SI
  | S n => let x := srefl (g1 n) : seq (g1 n) (g2 n) in g2 n
  end
with g2 (n:nat) : STrue :=
  match n with
  | 0 => SI
  | S n => let x := srefl (g1 n) : seq (g1 n) (g2 n) in g1 n
  end.
Fixpoint h1 (n:nat) : STrue with h2 (n:nat) : STrue.
exact
(match n with
  | 0 => SI
  | S n => let x := srefl (h1 n) : seq (h1 n) (h2 n) in h2 n
  end).
exact
(match n with
  | 0 => SI
  | S n => let x := srefl (h1 n) : seq (h1 n) (h2 n) in h1 n
  end).
Defined.
Theorem k1 (n:nat) : STrue with k2 (n:nat) : STrue.
exact
(match n with
  | 0 => SI
  | S n => let x := srefl (k1 n) : seq (k1 n) (k2 n) in k2 n
  end).
exact
(match n with
  | 0 => SI
  | S n => let x := srefl (k1 n) : seq (k1 n) (k2 n) in k1 n
  end).
Defined.

End FixpointRelevance.

Module ClearFixBody.

CoInductive Stream : Set := Cons : nat -> Stream -> Stream.

Section S.
#[clearbody] Let CoFixpoint f : Stream := Cons 1 f.
#[clearbody] Let Fixpoint g n := match n with 0 => 0 | S n => g n end.
Goal True.
Fail Check eq_refl : f = cofix f := Cons 1 f.
Fail Check eq_refl : g = fix g n := match n with 0 => 0 | S n => g n end.
Abort.
End S.

End ClearFixBody.

Module TheoremWithUnivs.

Fail Fixpoint f@{u} (n:nat) : nat with g@{v} (n:nat) : nat.
Fail Theorem f@{u} (n:nat) : nat with g@{v} (n:nat) : nat.
Fail CoFixpoint f@{u} (n:nat) : Stream 0 with g@{v} (n:nat) : Stream 0.
Succeed Fixpoint f@{u} (n:nat) : nat with g@{u} (n:nat) : nat.
Succeed Theorem f@{u} (n:nat) : nat with g@{u} (n:nat) : nat.
Succeed CoFixpoint f@{u} (n:nat) : Stream 0 with g@{u} (n:nat) : Stream 0.
Succeed Fixpoint f@{u} (n:nat) : nat with g (n:nat) : nat. (* Accepted *)
Succeed Theorem f@{u} (n:nat) : nat with g (n:nat) : nat. (* Accepted *)
Succeed CoFixpoint f@{u} (n:nat) : Stream 0 with g (n:nat) : Stream 0. (* Accepted *)

End TheoremWithUnivs.

Module DependMutualFix.

Inductive tree (A : Type) := Node : A -> list (tree A) -> tree A.

Definition lmap' {A B} (f : A -> B) : list A -> list B :=
fix F l :=
match l with
| nil => nil
| cons x l => cons (f x) (G l)
end
with G l :=
match l with
| nil => nil
| cons x l => cons (f x) (F l)
end for F.

(* Not yet able to accept this *)
Fail Fixpoint map {A B} (f : A -> B) (t : tree A) {struct t} : tree B :=
match t with
| Node _ x l => Node _ (f x) (lmap' (map f) l)
end.

End DependMutualFix.

Module Wish16040.

Inductive tree (A : Type) := Node : A -> list (tree A) -> tree A.

Fixpoint lmap {A B} (f : A -> B) (l : list A) : list B :=
match l with
| nil => nil
| cons x l => cons (f x) (lmap f l)
end.

Fixpoint map {A B} (f : A -> B) (t : tree A) {struct t} : tree B :=
match t with
| Node _ x l => Node _ (f x) (lmap (map f) l)
end.

(* Check that we don't find too much uniform parameters *)

Fixpoint lmap' {A} (f g : A -> A) (l : list A) : list A :=
match l with
| nil => nil
| cons x l => cons (f x) (lmap' g f l)
end.

(* Not supposed to be detected guarded, as only A is uniform in lmap' *)
Fail Fixpoint map' {A} (f : A -> A) (t : tree A) {struct t} : tree A :=
match t with
| Node _ x l => Node _ (f x) (lmap' (map' f) (map' f) l)
end.

(* Uniform arguments after a non-uniform one *)

Fixpoint lmap'' {A} n (f : A -> A) (l : list A) : list A :=
match l with
| nil => nil
| cons x l => cons (f x) (lmap'' (S n) f l)
end.

(* The current guard supports extrusion of uniform arguments only in prefix position *)
Fail Fixpoint map'' {A} (f : A -> A) (t : tree A) {struct t} : tree A :=
match t with
| Node _ x l => Node _ (f x) (lmap'' 0 (map'' f) l)
end.

End Wish16040.

Module TheoremWith.

CoInductive Stream : Set := Cons : nat -> Stream -> Stream.

(* Support for mutually recursive theorems in non-mutual types *)
Theorem a : Stream with b : Stream.
Proof.
apply (Cons 0), b.
apply (Cons 0), a.
Defined.

Theorem c (n:nat) : Stream with d (n:nat) : Stream. (* corecursive *)
Proof.
apply (Cons n), (d n).
apply (Cons n), (c n).
Defined.

Theorem c' (n:nat) : Stream with d' (n:nat) : Stream. (* recursive *)
Proof.
destruct n as [|n']. apply a. apply (d' n').
destruct n as [|n']. apply a. apply (c' n').
Defined.

End TheoremWith.

Module HighlyNested.

Inductive T A := E : A * list A * list (list A) -> T A.
Inductive U := H : T (T U) -> U.

Definition map {A B : Type} (f : A -> B) :=
  fix map (l : list A) : list B :=
  match l with
  | nil => nil
  | cons a t => cons (f a) (map t)
  end.

Definition mapT {A B} (f:A -> B) t :=
  match t with E _ (a, l, ll) => E _ (f a, map f l, map (map f) ll) end.

Fixpoint mapU (f:U->U) u :=
  match u with
  | H t => H (mapT (mapT (mapU f)) t)
  end.

End HighlyNested.

Module TestIntersection.

(* This example used to stress rtree.inter (3 nested types) *)

Inductive Pmap_ne (A : Type) :=
| PNode010 : A -> Pmap_ne A
| PNode110 : Pmap_ne A -> A -> Pmap_ne A.
Arguments PNode010 {A} _ : assert.
Arguments PNode110 {A} _ _ : assert.

Variant Pmap (A : Type) := PEmpty : Pmap A | PNodes : Pmap_ne A -> Pmap A.
Arguments PEmpty {A}.
Arguments PNodes {A} _.

Definition Pmap_ne_case {A B} (t : Pmap_ne A) (f : Pmap A -> option A -> Pmap A -> B) : B :=
  match t with
  | PNode010 x => f PEmpty (Some x) PEmpty
  | PNode110 l x => f (PNodes l) (Some x) PEmpty
  end.
Definition Pmap_fold_aux {A B} (go : B -> Pmap_ne A -> B) (y : B) (mt : Pmap A) : B :=
  match mt with PEmpty => y | PNodes t => go y t end.
Definition Pmap_ne_fold {A B} (f : A -> B -> B) : B -> Pmap_ne A -> B :=
  fix go y t :=
    Pmap_ne_case t (fun ml mx mr => Pmap_fold_aux go
      (Pmap_fold_aux go match mx with None => y | Some x => f x y end ml) mr).
Definition Pmap_fold {A} {B} (f : A -> B -> B) := Pmap_fold_aux (Pmap_ne_fold f).

Inductive test := Test : Pmap test -> test.
Fixpoint test_size (t : test) : nat :=
  let 'Test ts := t in S (Pmap_fold (fun t' => plus (test_size t')) 0%nat ts).

End TestIntersection.

quality95%

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