The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Hi Agnishom,

The problem you encounter at the end of Method1.v is that Fixpoints only reduce if the argument marked as structurally decreasing is a constructor. So your problem could be "minimized" as follows:

Fixpoint my_add(n m: nat) {struct n}: nat :=

  match m with

  | O => n

  | S m' =>

    match n with

    | O => m

    | S n' => S (S (my_add n' m'))

  end

end.

Goal forall x, my_add x 0 = x.

  intros. Fail reflexivity. simpl. (* doesn't simplify *)

Abort.

In your Method1.v, you could work around the problem by replacing the arbitrary acc you pass to decode_aux with a transparently-defined (rbc_lt_wf _), which you already do in decode_aux1, and proving the lemma for this one works as expected:

Lemma decode_aux1_eps (bc : list bool) :

  decode_aux1 Epsilon bc = Some (parse_epsilon, bc).

Proof.

  unfold decode_aux1. simpl. reflexivity.

Qed.

Best,

Sam

-----Original Message-----

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>

Reply-To: coq-club AT inria.fr

To: coq-club AT inria.fr

Subject: [Coq-Club] Why are my terms not reducing?

Date: 01/17/2024 05:40:33 PM

Hi Coq-club;

I recently came across the proof pearl titled "Well-founded recursion done right" by Xavier Leroy, and considered applying it to a proof I previously tried to attempt.

I wish to define the function described in this Haskell program, and I have tried three different approaches.

Approach 1(Method1.v) : This uses the mentioned proof-pearl. In this case, the _expression_ refuses to reduce.

Approach 2(Method2.v): Uses the refine tactic and this technique (from Pit-Claudel) to get rid of opaque proofs. Much of this code is thanks to Mukesh Tiwari. However, even in this case, the _expression_ refuses to reduce.

Approach 3(GitHub Issue): Uses the Equations package. This crashes coqtop.

Any ideas on why these refuse to reduce? In Page 2 of the proof-pearl, the author says "Now, the hole [...] is any proof of [...],and it can be opaque.". So, I assume that the error is not due to me providing opaque proofs.

--Agnishom