Mukesh Tiwari (Jun 05 2022 at 14:02): Mukesh Tiwari (Jun 05 2022 at 14:02):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.
Mukesh Tiwari (Jun 05 2022 at 14:19):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).
Li-yao (Jun 05 2022 at 14:29):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.
Mukesh Tiwari (Jun 05 2022 at 16:10):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.
Paolo Giarrusso (Jun 05 2022 at 18:46):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
Paolo Giarrusso (Jun 05 2022 at 18:47):dunno if that's needed, but it's not too surprising because of the le_n n : n <= n constructor.
Mukesh Tiwari (Jun 06 2022 at 18:09):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?
Paolo Giarrusso (Jun 06 2022 at 18:10):Well, _bugs_ in dependent elimination would create inconsistencies
Paolo Giarrusso (Jun 06 2022 at 18:12):that part isn't so different from adding anything to the kernel — but in fact there are extra questions
Paolo Giarrusso (Jun 06 2022 at 18:16):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.
Paolo Giarrusso (Jun 06 2022 at 18:20):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
Mukesh Tiwari (Jun 06 2022 at 18:23):Then it seems keeping Equations machinery out of the kernel is good idea.
Meven Lennon-Bertrand (Jun 07 2022 at 08:21):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
Paolo Giarrusso (Jun 07 2022 at 11:49):That would imply that moving across Coq and Agda might change the available def. equalities, which seems surprising...
Paolo Giarrusso (Jun 07 2022 at 11:53):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) Paolo Giarrusso (Jun 07 2022 at 11:57):Hm, that's claimed to be an example of a different problem with this translation https://twitter.com/aspiwack/status/1394012841951338504
You're happy for a while. But as people start to use recursive functions, they start complaining that performance is not great. Sometimes you just can't compile a recursive function to rec combinators while preserving the computational complexity. 14/30
- Arnaud Spiwack (@aspiwack) Meven Lennon-Bertrand (Jun 07 2022 at 12:44):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)
Meven Lennon-Bertrand (Jun 07 2022 at 12:47):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.
Notification Bot (Jun 19 2022 at 07:36):Mukesh Tiwari has marked this topic as resolved.
Last updated: May 28 2023 at 18:29 UTC