Inductively definite dense vector lemmas
Inspired by another question on StackOverflow, I defined a dense vector as a vector with elements of type option A
that only contains elements Some _
, not None
.
Require Import Vector.
Section Dense.
Variable A:Type.
Inductive Is_dense : forall n, t (option A) n -> Prop :=
| snil : Is_dense 0 (nil _)
| scons: forall n s, Is_dense n s -> forall a, Is_dense (S n) (cons _ (Some a) _ s).
How can I prove the following two lemmas:
Lemma Is_dense_tl: forall n (s: t (option A) (S n)),
Is_dense (S n) s -> Is_dense n (tl s).
and
Lemma dense_hd: forall n (s: t (option A) (S n)), Is_dense (S n) s -> A.
And also in the first lemma, when I do inversion s.
, I get the elements h n' X
that were used by the constructor s
, but how can I get the equality indicating s = cons (option A) h n' X
?
source to share
Due to the type dependency, inversion
it cannot directly generate what you expect, because it is not generally the case. However, this is true for a large family of types whose equality is decidable. In your case, you can apply Eqdep_dec.inj_pair2_eq_dec
to get the equality you want if you assert that equality is not nat
decidable (and it is).
Here is the proof of the first lemma:
Lemma Is_dense_tl: forall n (s: t (option A) (S n)),
Is_dense (S n) s -> Is_dense n (tl s).
Proof.
intros n s hs.
inversion hs; subst; clear hs.
apply Eqdep_dec.inj_pair2_eq_dec in H0.
- now rewrite <- H0; simpl.
- (* insert proof of decidablity *) admit.
Qed.
EDIT: About your comment on the second lemma.
The main difference between your two lemmas is that the first tries to prove the property Is_dense n (tl s)
that lives in Prop
, while the second tries to show the type term A
. In short, the former creates a genus term Prop
, the latter a genus term Type
.
To avoid inconsistencies in Coq logic, there is a hierarchy for organizing sorts, which (not really, but to give you a rough idea) Prop: Set
Set:Type_0
and Type_n: Type_n+1
. At the top of this hierarchy, a type system is built in which the dependent pair (for example, the type {n: nat | even n }
is the type of even natural numbers) is limited. You can build Prop
from another Prop
(e.g. forall p:Prop, p -> p
lives in Prop
). However, you need to be careful when involved Type
. For example, (again, please refer to Coq documentation for exact instructions) forall n:Type_i, Type_j
is of type Type_max(i,j)
.
This limitation is here to avoid inconsistency (eg Russell's paradox) in a Coq type system.
In your case, you are trying to check (using inversion
) the term sort Prop
( Is_dense (S n) s
) to construct a type term A
, sort Type
. This is prohibited by the type system. To build the sort term Type
, you need to check the conditions for at least the sort Set
. In your example, all you have to do is change the definition Is_dense
to land in Type
instead Prop
and you're good to go.
source to share