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
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
Equations' tactics are much better at avoiding axiom K
(Equations = the Coq-Equations library/Coq plugin)
Vector without using Coq-Equations is typically discouraged.
in part because of errors like the one you see
Last updated: Feb 04 2023 at 22:29 UTC