Skip to content

Instantly share code, notes, and snippets.

@anton-trunov
Created September 19, 2017 15:35
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anton-trunov/774fae6872df8d10a0350b73f326b1f4 to your computer and use it in GitHub Desktop.
Save anton-trunov/774fae6872df8d10a0350b73f326b1f4 to your computer and use it in GitHub Desktop.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.
Lemma forw_rev_list_ind {A}
(P : list A -> Prop)
(Pnil : P [])
(Psingle : (forall a, P [a]))
(Pmore : (forall a b, forall xs, P xs -> P ([a] ++ xs ++ [b])))
(xs : list A)
: P xs.
Proof.
induction xs as [xs IHxs] using (induction_ltof1 _ (@length _)); unfold ltof in IHxs.
destruct xs as [|x xs _] using rev_ind; [|destruct xs].
- exact Pnil.
- apply Psingle.
- apply Pmore, IHxs.
rewrite app_length; auto with arith.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment