The Coq mailing list

[Jason Hu <fdhzs2010 AT hotmail.com>]

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