Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement