The Coq mailing list

[Yves Bertot <yves.bertot AT inria.fr>]

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.