Stream: Coq users

Topic: Destruct terms of indexed types

Rudy Peterson (Feb 20 2022 at 23:26):

Hello!

I've been looking into the proof of of_list_to_list_opp in the vector library trying to understand how it is proved without the axiom eq_rect_eq and I see it uses case0.

I was attempting to prove case0 on my own with tactics rather than by explicitly constructing a proof term as done in the standard library, but whenever I tried to destruct v : VectorDef.t A 0 I kept running into the error:

Error: Abstracting over the terms "n" and "v" leads to a term
λ (n0 : ℕ) (v0 :  VectorDef.t A n0) ⇒ v0 = []
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "VectorDef.t A n0" : "Set"
 "v0" : "VectorDef.t A n0"
 "[]" : "VectorDef.t A 0"
The 3rd term has type "VectorDef.t A 0" which should be coercible to "VectorDef.t A n0".

Is there a way to destruct terms of dependent types without appealing to tactics that use axioms such as dependent destruction?

Thanks!

Paolo Giarrusso (Feb 21 2022 at 01:07):

Equations' tactics are much better at avoiding axiom K

Paolo Giarrusso (Feb 21 2022 at 01:08):

(Equations = the Coq-Equations library/Coq plugin)

Paolo Giarrusso (Feb 21 2022 at 01:09):

moreover, using Vector without using Coq-Equations is typically discouraged.

Paolo Giarrusso (Feb 21 2022 at 01:10):

in part because of errors like the one you see

Last updated: Oct 01 2023 at 19:01 UTC