The Coq mailing list

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

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.