Stream: MetaCoq

Topic: Lack of decidable equality


view this post on Zulip Jason Gross (Nov 01 2022 at 12:47):

Argh, why does MetaCoq use a representation of term Asts where equality is not decidable?

view this post on Zulip Théo Winterhalter (Nov 01 2022 at 12:55):

Why is it not?

view this post on Zulip Jason Gross (Nov 01 2022 at 12:57):

It's not entirely clear to me that the bst proofs for AVL trees satisfy proof irrelevance. (I guess they might, which would probably be enough)

view this post on Zulip Jason Gross (Nov 01 2022 at 12:58):

But deciding equality of typing derivations is hopeless, because they contain exists v : valuation, ... -> ...

view this post on Zulip Théo Winterhalter (Nov 01 2022 at 12:59):

Ah so it's not about ASTs then right?

view this post on Zulip Jason Gross (Nov 01 2022 at 13:03):

Ah, yeah, I guess I don't actually need to decide equality of typing derivations, only term asts. And I guess it's a bit annoying that Scheme Equality doesn't work on term ASTs, but I can work around it

view this post on Zulip Jason Gross (Nov 01 2022 at 19:46):

Actually, nope, I don't think equality of term Asts is decidable

view this post on Zulip Jason Gross (Nov 01 2022 at 19:48):

Essentially I need to prove

forall (P Q : Prop)
            (P_hProp : forall x y : P, x = y) (Q_hProp : forall x y : Q, x = y)
            (PQ_incompat1 : P -> ~Q) (PQ_incompat2 : Q -> ~P)
            (dec : P \/ Q -> {P} + {Q})
            (a b : P \/ Q),
    a = b.

(instead of or I have MSetAVL.Raw.bst, but it's basically the same problem), and I don't think this is doable.

view this post on Zulip Jason Gross (Nov 01 2022 at 19:49):

Or even more simply, forall (P Q : Prop) (pq : P \/ Q) (p : P) (P_hProp : forall p', p' = p), ~Q -> pq = or_introl p.

view this post on Zulip Gaëtan Gilbert (Nov 01 2022 at 20:19):

it's very doable

Lemma foo (P Q : Prop)
  (P_hProp : forall x y : P, x = y) (Q_hProp : forall x y : Q, x = y)
  (PQ_incompat1 : P -> ~Q) (PQ_incompat2 : Q -> ~P)
  (dec : P \/ Q -> {P} + {Q})
  (a b : P \/ Q)
  : a = b.
Proof.
  destruct a,b.
  1,4:f_equal;auto.
  all:destruct PQ_incompat1;assumption.
Qed.

view this post on Zulip Gaëtan Gilbert (Nov 01 2022 at 20:20):

also you don't need dec and one of the PQ_incompat (they are equivalent)

view this post on Zulip Jason Gross (Nov 01 2022 at 20:30):

Huh, I thought Prop elimination forbid that destruct?

view this post on Zulip Jason Gross (Nov 01 2022 at 20:37):

Gr, okay, even with that fact (thanks @Gaëtan Gilbert ), equality is still not decidable without function extensionality because MSetAVL and FMapAVL use forall y : M.Raw.key, M.Raw.In y m -> T.lt y x for lt_tree and gt_tree, which means that the bst proof carries functions :-(

view this post on Zulip Jason Gross (Nov 01 2022 at 20:48):

Note, btw, that this means that getting a reflective version of Ast.declared_constructor is impossible (follow the chain of definitions Ast.Env.mutual_inductive_body, Template.Universes.universes_decl, Template.Universes.AUContext.t, Template.Universes.ConstraintSet.t)

view this post on Zulip Gaëtan Gilbert (Nov 01 2022 at 21:02):

Jason Gross said:

Huh, I thought Prop elimination forbid that destruct?

eq is a prop

view this post on Zulip Jason Gross (Nov 01 2022 at 21:03):

Yes, I was thinking that we'd end up needing a match in the return clause that performed a forbidden elimination.

view this post on Zulip Gaëtan Gilbert (Nov 01 2022 at 21:06):

we could change lt/gt_tree to use an inductive Forall instead of forall+In

view this post on Zulip Jason Gross (Nov 01 2022 at 21:57):

That would be great! But wouldn't that break a bunch of backwards compat stuff? (Or are you talking about vendoring a copy in MetaCoq?)

view this post on Zulip Gaëtan Gilbert (Nov 01 2022 at 21:57):

idk how much stuff relies on how this stuff is defined

view this post on Zulip Jason Gross (Nov 01 2022 at 21:58):

I guess Coq's CI could tell us

view this post on Zulip Théo Winterhalter (Nov 02 2022 at 09:13):

But we have a decision procedure here: https://github.com/MetaCoq/metacoq/blob/coq-8.16/pcuic/theories/Syntax/PCUICReflect.v#L196

view this post on Zulip Théo Winterhalter (Nov 02 2022 at 09:14):

We use mainly (only?) to get UIP on it. Indeed, the equality on terms we care about is modulo names and universes.

view this post on Zulip Jason Gross (Nov 02 2022 at 13:59):

That's an equality decision procedure for term, though, which AIUI doesn't include decls for universes, constraints, and things like mutual_inductive_body, right? I'm looking for an equality decision procedure for environments, so that I can reflectively instantiate the various preconditions of the typing constructors.

view this post on Zulip Jason Gross (Nov 02 2022 at 14:00):

I guess I could have a reflective version that spits out a modified env replacing all the non-decidable parts with the versions I'm looking for and then have the reflection prove a single equality of envs, but this seems a bit unfortunate.

view this post on Zulip Théo Winterhalter (Nov 02 2022 at 14:17):

Ah, I misunderstood what you wanted. But yeah, for stuff like mutual_inductive_body I think we never had to worry about them being equal or not.

view this post on Zulip Jason Gross (Nov 02 2022 at 19:48):

It looks like reflect_mutual_inductive_body is defined but commented out at https://github.com/MetaCoq/metacoq/blob/d702f18ce289530cdd0be3d0ad331cb1ad38f6a0/template-coq/theories/ReflectAst.v#L214?

view this post on Zulip Jason Gross (Nov 02 2022 at 19:49):

And it was commented out by @Matthieu Sozeau with the switch to AVLs... https://github.com/MetaCoq/metacoq/commit/13f91e635a1b0cf27db4a70c051661c66133eb61

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 21:52):

Ah, maybe because the useful AVL equality isn't Leibniz equality: that last commit switches from equality to ConstraintSet.Equal in one place

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 22:01):

Indeed, https://github.com/MetaCoq/metacoq/pull/644 points out that "AVL equality isn't Leibniz" is the main downside. You could lift AVL equivalence, or switch to an efficient tree that is still Leibniz (stdpp's gmap should qualify, but it has overhead before extraction; Appel's recent tries do better and could replace stdpp.pmap, but they still need stdpp.gmap to deal with arbitrary countable key types.

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:49):

Yes, that's an unfortunate issue. Maybe there's a workaround using a decidable is_bst function though?

view this post on Zulip Jason Gross (Nov 23 2022 at 13:47):

@Matthieu Sozeau do you mean using a variant of MSet/FMap that bakes in a proof using the is_bst function? Or storing in the term AST a raw tree + a proof of is_bst = true and having coercions to the normal tree type? Or something else?

view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 11:29):

I guess the second solution. We should first benchmark if the canonical tries provide enough performance I guess, that would simplify the formalization.


Last updated: Mar 29 2024 at 13:01 UTC