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

Why is it not?

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)

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

Ah so it's not about ASTs then right?

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

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

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.

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

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

also you don't need `dec`

and one of the PQ_incompat (they are equivalent)

Huh, I thought `Prop`

elimination forbid that destruct?

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

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`

)

Jason Gross said:

Huh, I thought

`Prop`

elimination forbid that destruct?

eq is a prop

Yes, I was thinking that we'd end up needing a `match`

in the `return`

clause that performed a forbidden elimination.

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

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

idk how much stuff relies on how this stuff is defined

I guess Coq's CI could tell us

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

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

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.

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.

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.

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?

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

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

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.

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

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

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: Dec 01 2023 at 07:01 UTC