Skip to content

Instantly share code, notes, and snippets.

@davidad

davidad/vec_rev_involutive.v

Last active July 12, 2018 22:13
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save davidad/6a81697206ded0ee628a492eb4c0458b to your computer and use it in GitHub Desktop.
Save davidad/6a81697206ded0ee628a492eb4c0458b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
vec_rev_involutive.v
Require Import Coq.Lists.List Coq.Logic.Eqdep.
Definition vec (A: Type) (n: nat) : Type := {l: list A | length l = n}.
Section vec_rev.
Variable A : Type.
Variable n : nat.
Definition vec_rev (l: vec A n): vec A n.
Proof.
refine (exist _ (rev (proj1_sig l)) _).
destruct l; rewrite rev_length; trivial.
Defined.
Lemma vec_rev_involutive: forall l, vec_rev (vec_rev l) = l.
Proof.
intro; unshelve eapply eq_sig.
- apply rev_involutive.
- apply UIP.
Qed.
End vec_rev.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment