Stream: Coq users

Topic: Destruct terms of indexed types


view this post on Zulip 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!

view this post on Zulip Paolo Giarrusso (Feb 21 2022 at 01:07):

Equations' tactics are much better at avoiding axiom K

view this post on Zulip Paolo Giarrusso (Feb 21 2022 at 01:08):

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

view this post on Zulip Paolo Giarrusso (Feb 21 2022 at 01:09):

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

view this post on Zulip Paolo Giarrusso (Feb 21 2022 at 01:10):

in part because of errors like the one you see


Last updated: Feb 04 2023 at 22:29 UTC