logo
down
shadow

Nested recursion and `Program Fixpoint` or `Function`


Nested recursion and `Program Fixpoint` or `Function`

By : Geoff Huston
Date : November 21 2020, 03:00 PM
hope this fix your issue In general, it might be advisable to avoid this problem. But if one really wants to obtain the proof obligation that Isabelle gives you, here is a way:
In Isabelle, we can give an external lemma that stats that map applies its arguments only to members of the given list. In Coq, we cannot do this in an external lemma, but we can do it in the type. So instead of the normal type of map
code :
forall A B, (A -> B) -> list A -> list B
forall A B (xs : list A), (forall x : A, In x xs -> B) -> list B
Definition map {A B} (xs : list A) (f : forall (x:A), In x xs -> B) : list B.
Proof.
  induction xs.
  * exact [].
  * refine (f a _ :: IHxs _).
    - left. reflexivity.
    - intros. eapply f. right. eassumption.
Defined.
Fixpoint map {A B} (xs : list A) : forall (f : forall (x:A), In x xs -> B), list B :=
  match xs with
   | [] => fun _ => []
   | x :: xs => fun f => f x (or_introl eq_refl) :: map xs (fun y h => f y (or_intror h))
  end.
Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map ts (fun t _ => mapTree f t))
  end.
Next Obligation.
  simpl.
  apply Lt.le_lt_n_Sm.
  induction ts; inversion_clear H.
  - subst. apply PeanoNat.Nat.le_max_l.
  - rewrite IHts by assumption.
    apply PeanoNat.Nat.le_max_r.
Qed.


Share : facebook icon twitter icon
Coq simpl for Program Fixpoint

Coq simpl for Program Fixpoint


By : archana
Date : March 29 2020, 07:55 AM
I think the issue was by ths following , I'm not used to using Program so there's probably a better solution but this is what I came up with by unfolding bla, seeing that it was internally defined using Fix_sub and looking at the theorems about that function by using SearchAbout Fix_sub.
code :
Lemma obvious: forall n, bla n = n.
Proof.
intro n ; induction n.
 reflexivity.
 unfold bla ; rewrite fix_sub_eq ; simpl ; fold (bla n).
 rewrite IHn ; reflexivity.

(* This can probably be automated using Ltac *)
 intros x f g Heq.
  destruct x.
  reflexivity.
  f_equal ; apply Heq.
Qed.
Lemma blaS_red : forall n, bla (S n) = S (bla n).
Proof.
intro n.
 unfold bla ; rewrite fix_sub_eq ; simpl ; fold (bla n).
 reflexivity.

(* This can probably be automated using Ltac *)
 intros x f g Heq.
  destruct x.
  reflexivity.
  f_equal ; apply Heq.
Qed.
What's the difference between Program Fixpoint and Function in Coq?

What's the difference between Program Fixpoint and Function in Coq?


By : Dan Poulos
Date : March 29 2020, 07:55 AM
Does that help This may not be a complete list, but it is what I have found so far:
As you already mentioned, Program Fixpoint allows the measure to look at more than one argument. Function creates a foo_equation lemma that can be used to rewrite calls to foo with its RHS. Very useful to avoid problems like Coq simpl for Program Fixpoint. In some (simple?) cases, Function can define a foo_ind lemma to perform induction along the structure of recursive calls of foo. Again, very useful to prove things about foo without effectively repeating the termination argument in the proof. Program Fixpoint can be tricked into supporting nested recursion, see https://stackoverflow.com/a/46859452/946226. This is also why Program Fixpoint can define the Ackermann function when Function cannot.
Decreasing argument (and what is a Program Fixpoint)

Decreasing argument (and what is a Program Fixpoint)


By : შალვა დოლიაშვილი
Date : March 29 2020, 07:55 AM
I think the issue was by ths following ,
The Fixpoint command in Coq constructs a recursive function using Coq's primitive fix, which checks for structural recursion to ensure termination. This is the only recursion in Coq, and all other techniques ultimately desugar to a fix of some sort.
code :
Nat.add = 
  fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end : nat -> nat -> nat
Destruct if condition in program fixpoint coq

Destruct if condition in program fixpoint coq


By : 1376858
Date : March 29 2020, 07:55 AM
With these it helps Program gives you terms that are difficult to work with, so you should prove a lemma that factor is equal to its body, and then rewrite with that, instead of unfolding. (I used match instead of if to get hold of the dvd proof term.)
code :
Lemma factor_lemma a b agt0 bgt1:
  factor a b agt0 bgt1 =
  match Zdivide_dec b a with
  | left dvd => 1+factor (a/b) b (divgt0 a b agt0 bgt1 dvd)  bgt1
  | right notdvd =>  0 end.
Proof.
  unfold factor at 1.
  unfold factor_func; rewrite Program.Wf.Fix_eq; fold factor_func.
  - reflexivity.
  - intros.
    destruct Zdivide_dec; auto.
    congruence.
Qed.
Lemma factor_div ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) : (b ^ (factor a b agt0 bgt1) | a).
Proof.
  rewrite factor_lemma.
  destruct Zdivide_dec.

  2:   now rewrite Z.pow_0_r;apply Z.divide_1_l.
  a, b : Z
  agt0 : 0 < a
  bgt1 : 1 < b
  d : (b | a)
  ============================
  (b ^ (1 + factor (a / b) b (divgt0 a b agt0 bgt1 d) bgt1) | a)
Fixpoint proofs with a nested induction on the value of a function

Fixpoint proofs with a nested induction on the value of a function


By : Taimoor Khalid
Date : March 29 2020, 07:55 AM
should help you out To use nested recursion you have to resort to the raw fix construct using the "fix 1" tactic for example. The induction principles won't give you the right recursive calls. Beware that inversions might do rewritings that confuse the guard checker.
Actually, if you want the "nested" fixpoint to not be on a subterm of the original list but on [dfs t] then it's no longer a structural recursion and you need to justify the recursion using well-founded recursion. I have a similar example on rose trees where well-founded nested recursion is used.
shadow
Privacy Policy - Terms - Contact Us © voile276.org