I am using Equations package to write this proof `le_unique`

which the type checker happily accepts and display the message `Equations definition le_unique is complete and requires no further proofs. Use the "Equations" command to define it.`

but the moment I get rid of `?`

it immediately complains about `Recursive definition of le_unique is ill-formed.`

Is this a bug in the package or something is wrong with my code?

```
From Equations Require Import Equations.
Set Equations With UIP.
Lemma inj_le_S :
forall (p n : nat) (Ha Hb : p <= n),
Ha = Hb -> le_S p n Ha = le_S p n Hb.
Proof.
intros * Heq.
f_equal.
exact Heq.
Defined.
Equations?
le_unique {p n : nat}
(h h' : p <= n) : h = h' :=
le_unique (le_n Ha) (le_n Hb) := eq_refl;
le_unique (le_n Ha) (le_S _ _ Hb) := _ ;
le_unique (le_S _ _ Ha) (le_n Hb) := _;
le_unique (le_S p pa Ha) (le_S p pa Hb) :=
inj_le_S p pa Ha Hb (le_unique Ha Hb).
```

You get the same error message if you try to actually close the `Equations?`

definition with `Defined`

.

Yes, I am getting the same error message with `Defined`

as well, but I don't understand what is wrong with my proof. Based on my understanding, the recursive call is on smaller argument (the error message is difficult to parse and understand).

The desugaring of equations to Gallina is nontrivial. The error message shows the resulting fixpoint, where `le_unique`

is applied to a `fun`

parameter, and not the result of pattern-matching on `h`

.

Thanks @Li-yao . Now I managed to take a step in the direction I wanted, but I am still far from the proof. I realised that `le_ind`

is useless so I used `Scheme`

to get one that works for me.

```
Scheme le_indd := Induction for le Sort Prop.
Lemma le_unique : forall {m n : nat}
(p q : m <= n), p = q.
Proof.
induction p using le_indd.
+ intros Hq.
admit.
+ intros Hq.
```

I just shifted the goal post :) .

Edit: Finally proved it.

```
Lemma le_pair_induction:
forall (n : nat)
(P : forall m : nat, n <= m -> n <= m -> Prop),
P n (le_n n) (le_n n) ->
(forall (m : nat) (Ha Hb : n <= m), P m Ha Hb ->
P (S m) (le_S n m Ha) (le_S n m Hb)) ->
forall (mt : nat) (Hna Hnb : n <= mt), P mt Hna Hnb.
Proof.
intros ? ? Pa Pb.
refine(
fix Fn mt Hna {struct Hna} :=
match Hna as Hna' in (_ <= mtp)
return
mt = mtp ->
forall Hnb, P mtp Hna' Hnb
with
| le_n _ => fun Hna Hnb =>
match Hnb as Hnb' in (_ <= nt)
return
forall (pf : nt = n),
P n (le_n n) (eq_rect nt _ Hnb' n pf)
with
| le_n _ => fun pf => _
| le_S _ nt Hnt => fun pf => _
end eq_refl
| le_S _ nt Hnt => fun Heq Hnb =>
match Hnb as Hnb' in (_ <= S np)
return
forall (pf : np = nt),
P (S nt) (le_S n nt Hnt)
(eq_rect np (fun w => n <= S w) Hnb' nt pf)
with
| le_n _ => _
| le_S _ nw Hnw => fun pf => _
end eq_refl
end eq_refl).
+ rewrite (uip_nat pf).
exact Pa.
+ abstract nia.
+ clear Fn.
destruct n.
++ exact idProp.
++ abstract nia.
+ subst.
apply Pb, Fn.
Qed.
Lemma le_uniquet : forall {m n : nat}
(p q : m <= n), p = q.
Proof.
intros ? ? ? ?.
apply (le_pair_indd m
(fun (n : nat) (a : m <= n) (b : m <= n) => a = b)).
+ exact eq_refl.
+ intros ? ? ? He;
subst; reflexivity.
Qed.
```

```
Require Import iris.prelude.prelude.
Require Import Equations.Prop.Equations.
Scheme le_indd := Induction for le Sort Prop.
Set Equations With UIP.
Derive EqDec NoConfusion NoConfusionHom for nat.
Derive Subterm for nat.
(* Fail Derive DependentEliminationPackage for nat.
(* Derive Signature for nat. *)
Derive Signature for Peano.le.
Fail Derive NoConfusionHom for Peano.le.
Fail Derive NoConfusion for Peano.le.
Fail Derive Eqdec for Peano.le.
Fail Derive Subterm for le.
Fail Derive DependentEliminationPackage for Peano.le. *)
Lemma le_unique : forall {m n : nat}
(p q : m <= n), p = q.
Proof.
induction p using le_indd.
+ intros Hq.
dependent elimination Hq; last lia.
done.
+ intros Hq.
dependent elimination Hq; first lia.
f_equal.
apply IHp.
Qed.
```

Minimized:

```
Require Import Lia.
Require Import Equations.Prop.Equations.
Scheme le_indd := Induction for le Sort Prop.
Set Equations With UIP.
Lemma le_unique : forall {m n : nat}
(p q : m <= n), p = q.
Proof.
induction p using le_indd.
+ intros Hq.
dependent elimination Hq; [|lia].
easy.
+ intros Hq.
dependent elimination Hq; [lia|].
f_equal.
apply IHp.
Qed.
Print Assumptions le_unique. (* Closed under the global context *)
```

I had misunderstood `Set Equations With UIP.`

— the proof requires it, but that flag is required to use provable UIP, not just for the axiom.

and even mathcomp's proof uses provable UIP (`eq_axiomK`

):

https://github.com/math-comp/math-comp/blob/55c796c6b7408575817612ba1b9ecde68e3a7d01/mathcomp/ssreflect/ssrnat.v#L474-L484

dunno if that's needed, but it's not too surprising because of the `le_n n : n <= n`

constructor.

Thanks @Paolo Giarrusso . Equations made this proof really a breeze. Also, how difficult it would be to put all the magic of 'dependent elimination` of Equations in Coq (kernel) itself? Would it create any inconsistency?

Well, _bugs_ in dependent elimination would create inconsistencies

that part isn't so different from adding anything to the kernel — but in fact there are extra questions

Essentially*, in Agda each equation you write holds as a definitional equality. I don't think Equations (or compiling to eliminators, in general) can give that guarantee. And in general, turning propositional equalities into definitional ones does not preserve all the metatheory (it preserves soundness, as shown by ETT, but it need not preserve e.g. decidable typechecking)

*For best results use `--exact-split`

.

many believe that the most sound strategy is to have the kernel only support eliminators, and compile to it any extensions, as done in Lean — both Agda's dependent pattern matching and Coq's support for general fixpoints + termination checking via the guard condition. That's also the strategy for the latest Coq soundness proof

Then it seems keeping Equations machinery out of the kernel is good idea.

Paolo Giarrusso said:

Essentially*, in Agda each equation you write holds as a definitional equality. I don't think Equations (or compiling to eliminators, in general) can give that guarantee. And in general, turning propositional equalities into definitional ones does not preserve all the metatheory (it preserves soundness, as shown by ETT, but it need not preserve e.g. decidable typechecking)

For case-trees -> eliminators (ie Agda), definitional equations are preserved (if I don’t misread Theorem 4.29 in Jesper Cockx’s PhD thesis). In the case of fix+match -> eliminators (ie Coq), the paper by Gimenez from the 90s seems to say the two are only propositionally but not definitionally equal, and then you indeed some meta-theory is lost

That would imply that moving across Coq and Agda might change the available def. equalities, which seems surprising...

Meanwhile, I'm no expert but what about https://twitter.com/aspiwack/status/1394331053511389186 ? I guess I should check what Equations produces here

@mietek Maybe Fixpoint divide_by_two (n : nat) := match n with | 0 => 0 | 1 => 0 | S (S n) => divide_by_two n end. Not sure, about this. But it's a bit tricky to compile it to combinators anyway.

- Arnaud Spiwack (@aspiwack)Hm, that's claimed to be an example of a different problem with this translation https://twitter.com/aspiwack/status/1394012841951338504

Paolo Giarrusso said:

Meanwhile, I'm no expert but what about https://twitter.com/aspiwack/status/1394331053511389186 ? I guess I should check what Equations produces here

I don’t know about Equations, but Gimenez and Cockx both do the same thing: they go through a datastructure encoding all possible recursive calls (basically, a generalization of strong induction on natural numbers)

Paolo Giarrusso said:

That would imply that moving across Coq and Agda might change the available def. equalities, which seems surprising...

It’s not very surprising to me that you do not get exactly the same definitional equations between both systems. After all, even slightly different definitions in Coq can have different equations, and afaict there is not one clear mapping from Coq’s syntax to Agda’s, so you are bound to hit this kind of small-but-subtle differences. But I guess nothing too important: on canonical inputs, both functions will probably give the same equations, the difficulties arise when you are stuck and do not exactly reduce in the same way on both sides.

Mukesh Tiwari has marked this topic as resolved.

Last updated: Apr 21 2024 at 01:02 UTC