The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thanks, I did not know about the with-pattern in Equations.

I tried using it here (the file Attempt1.v) : https://gist.github.com/Agnishom/a7414c092c1d23e37afebaa26f57580e#file-attempt1-v

But now I have a different problem. The last "Defined" seems to take about 10 seconds to finish and crashes Coq thereafter.

--Agnishom

On Tue, Nov 21, 2023 at 10:44 PM Jason Hu <fdhzs2010 AT hotmail.com> wrote:

why don't you use with-pattern? Convoy pattern should be automatic if you use with-pattern in Equations.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Sent: Tuesday, November 21, 2023 3:39 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] Non obvious recursion (Convoy Pattern + Sigma Types + Equations)

 

Hi Coq-Club;

The code for the minimal complete example can be found here: https://gist.github.com/Agnishom/a7414c092c1d23e37afebaa26f57580e

I want to define a function which decreases in one argument using < and on another structurally. However, this seems to be rather complex in this case because of two reasons:

(1) the proofs do not seem to remember the appropriate information when I use match

(2) when I have multiple recursive calls, I need to be able to propagate the hypothesis through each recursive call.

For (1), I learnt that the appropriate tool is the Convoy Pattern. For (2), my guess is that the appropriate solution is to use a return type of the form {x | P x} so that P is known at every step.

However, when I try to combine these things, I get some very unfriendly error messages. One example is this:

(unable to find a well-typed instantiation for "?P": cannot ensure that
	"match o0 with
	| Some p => let (_, btc) := p in length btc <= length (snd (f, btc'))
	| None => True
	end" is a subtype of
	"(fun o : option (parse_tree * list bool) =>
	match o with
	| Some p => let (_, btc) := p in length btc <= length (snd (f, btc'))
	| None => True
	end) (Some (t2, btc''))").

I believe that the issue arises from guessing an _ term incorrectly. But I am not sure that this is the case since I thought that Equations would make me prove any term that it is unsure about as an Obligation. 

Any help is appreciated.

Thanks.

--Agnishom