The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

Dear Ben,

Thanks for the suggestion. The program I am using also involves proofs of some terms. This I am currently doing by leaving proof holes and later proving them.

For example, Fixpoint test (x y:nat):some_type:=(refine match x with 0 => t1(x, y, _) | S n => t2(x, n, _) end). , where both the terms t1 and t2 require proofs _ which

I am proving later. Not very sure how to handle this.

Regards,

-Suneel

On Tue, Sep 6, 2022 at 12:21 PM D. Ben Knoble <ben.knoble AT gmail.com> wrote:

You might need `{measure}` from `FunInd`'s `Function`:
https://coq.inria.fr/refman/using/libraries/funind.html
This will require a proof that the measure function is decreasing in
recursive calls (I've used this before with a list that Coq could not
see shrinking, but whose length was smaller by 1 in recursive calls).
D. Ben Knoble

On Fri, Sep 2, 2022 at 1:42 PM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:
>
> Dear friend,
> Is there a way to write a fixpoint using a tree such that in each recursive call the tree after removing the minimum element is used?
> I am getting the following error.
>
> Require Import MSets MSetRBT ZArith.
> Module M := MSetRBT.Ops Nat_as_OT.
>
> Fixpoint test (tb ta : M.t)(a:M.elt) :M.t.
> destruct (M.remove_min tb) eqn:H.
> destruct p eqn:Hp.
> unfold M.elt in a.
> destruct (a-e) eqn:Hae.
> exact (test t ta a).
> exact ta.
> exact ta.
> Defined.
> (* Cannot guess decreasing argument of fix. *)
>
> Also the {struct tb} failed.
>
>