The Coq mailing list

[manoury <pascal.manoury AT lip6.fr>]

It works !

        Pascal.

> Le 28 oct. 2021 à 09:47, manoury <pascal.manoury AT lip6.fr> a écrit :
> 
> Thank you Yves for this pointer. It seems sound. I’ll try it and tell you 
> about the result.
> 
> Pascal.
> 
>> Le 27 oct. 2021 à 19:32, Yves Bertot <Yves.Bertot AT inria.fr> a écrit :
>> 
>> I had the same problem last week!
>> 
>> If you proved a statement of the form well_founded it is not sufficient.
>> You must add an instance in the class WellFounded.
>> 
>> See https://stackoverflow.com/a/69678500/1809211
>> 
>> You did not give enough information in your question, so I am not sure
>> this will be enough for you.
>> 
>> Yves
>> ----- Original Message -----
>>> From: "manoury" <pascal.manoury AT lip6.fr>
>>> To: "coq-club" <coq-club AT inria.fr>
>>> Sent: Wednesday, October 27, 2021 5:01:40 PM
>>> Subject: [Coq-Club] Equations by WellFounded ad hoc measure
>> 
>>> I defined for binary trees the following measure
>>> 
>>> --
>>> Definition bt_mesure {A:Set} (bt:btree A) : (nat * nat) :=
>>> match bt with
>>>  Empty => (0,0)
>>> | Node _ bt1 _ => (btree_size bt, btree_size bt1)
>>> end.
>>> —
>>> 
>>> where tree_size is the usual
>>> 
>>> --
>>> Fixpoint btree_size {A:Set} (bt:btree A) : nat :=
>>> match bt with
>>>  Empty => 0
>>> | Node x bt1 bt2 => S (btree_size bt1 + btree_size bt2)
>>> end.
>>> —
>>> 
>>> I proved that lexicographic ordering of pairs of natural (I call it 
>>> nat_lex_lt)
>>> is well founded.
>>> Then I try the following:
>>> 
>>> --
>>> Equations list_of_btree {A:Set} (bt:btree A) : (list A) by wf (bt_mesure 
>>> bt)
>>> nat_lex_lt :=
>>> list_of_btree Empty := nil;
>>> list_of_btree (Node x Empty bt) := x::(list_of_btree bt);
>>> list_of_btree (Node x1 (Node x2 bt1 bt2) bt3) :=
>>>  (list_of_btree (Node x1 bt1 (Node x2 bt2 bt3))).
>>> —
>>> 
>>> And I get the following:
>>> 
>>> --
>>> Error:
>>> Unable to satisfy the following constraints:
>>> 
>>> ?w : "WellFounded
>>>      (Telescopes.tele_measure
>>>         (Telescopes.ext Set (fun A : Set => Telescopes.tip (btree A)))
>>>         (nat * nat) (fun (A : Set) (bt : btree A) => bt_mesure bt) 
>>> nat_lex_lt)"
>>> —
>>> 
>>> Any hint ? Thanks !
>>> 
>>>     Pascal Manoury.
>