## Stream: MetaCoq

### Topic: Lack of decidable equality

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

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

Why is it not?

#### 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):

Ah so it's not about ASTs then right?

#### 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):

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

#### 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.

#### 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):

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.
``````

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

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

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

Huh, I thought `Prop` elimination forbid that destruct?

#### 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 said:

Huh, I thought `Prop` elimination forbid that destruct?

eq is a prop

#### 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):

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

#### 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):

idk how much stuff relies on how this stuff is defined

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

I guess Coq's CI could tell us

#### 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

#### 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):

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?

#### 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

#### 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.

Last updated: Feb 04 2023 at 02:03 UTC