The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

I rewrote my previous code using proof by reflection [1]. In the past, I used to get a bunch of theorems when I tried *Print Opaque Dependencies decode_aux.* but after rewriting it [2] I am nothing, except *Section Variables A : Type*.  Moreover,

I can compute with this function for the values that in the past used to stuck [3], but I can still not proof the theorem [4]:

Lemma decode_aux1_union_l (r1 r2 : Regex) (bc : list bool) :
    decode_aux1 (r1 ∪ r2) (false :: bc) =
    match decode_aux1 r1 bc with
    | Some (t, bc') => Some (parse_union_l t, bc')
    | None => None
    end.

 

Any idea how to get around this?

Best,

Mukesh

[1] https://gist.github.com/mukeshtiwari/4a392728bd9907fa3980b3ccbe5211eb

[2] https://gist.github.com/mukeshtiwari/4a392728bd9907fa3980b3ccbe5211eb#file-wf-v-L543

[3] https://gist.github.com/mukeshtiwari/4a392728bd9907fa3980b3ccbe5211eb#file-wf-v-L540 

[4] https://gist.github.com/mukeshtiwari/4a392728bd9907fa3980b3ccbe5211eb#file-wf-v-L551

On Wed, Jan 24, 2024 at 4:34 PM Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Thanks for the suggestion, Samuel.

Indeed, in the case of Epsilon, this seems to work. 

However, it seems that now my proofs depend on _which_ proof of accessibility I use. For example,

Definition decode_aux1 (e : Regex) (btc : list bool) : option (parse_tree * list bool) :=

decode_aux (e, btc) (rbc_lt_wf (e, btc)).

Lemma decode_aux_union_l (e1 e2 : Regex) (bc : list bool) (t : parse_tree) (bc' : list bool) :

(forall acc, decode_aux (e1, bc) acc = Some (t, bc')) ->

decode_aux1 (Union e1 e2) (false :: bc) = Some (parse_union_l t, bc').

Proof.

unfold decode_aux1.

intros.

simpl. (* the term explodes in size *)

rewrite H. reflexivity.

Qed.

Now, this works but it is not very helpful because the hypothesis here requires something that is universal in the accessibility proof.

On Mon, Jan 22, 2024 at 3:50 PM Samuel Gruetter <gruetter AT mit.edu> wrote:

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