Lack of decidable equality · MetaCoq

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

Théo Winterhalter (Nov 01 2022 at 12:55):

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)

Jason Gross (Nov 01 2022 at 12:58):

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

Théo Winterhalter (Nov 01 2022 at 12:59):

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

Jason Gross (Nov 01 2022 at 19:46):

Jason Gross (Nov 01 2022 at 19:48):

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.

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.

Gaëtan Gilbert (Nov 01 2022 at 20:19):

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.

Gaëtan Gilbert (Nov 01 2022 at 20:20):

Jason Gross (Nov 01 2022 at 20:30):

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 :-(

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)

Gaëtan Gilbert (Nov 01 2022 at 21:02):

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.

Gaëtan Gilbert (Nov 01 2022 at 21:06):

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?)

Gaëtan Gilbert (Nov 01 2022 at 21:57):

Jason Gross (Nov 01 2022 at 21:58):

Théo Winterhalter (Nov 02 2022 at 09:13):

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.

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.

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.

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.

Jason Gross (Nov 02 2022 at 19:48):

Jason Gross (Nov 02 2022 at 19:49):

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

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.

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?

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?

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.

Stream: MetaCoq

Topic: Lack of decidable equality

Jason Gross (Nov 01 2022 at 12:47):