Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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