diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IterList.v | 96 | ||||
| -rw-r--r-- | lib/OptionMonad.v | 49 |
2 files changed, 145 insertions, 0 deletions
diff --git a/lib/IterList.v b/lib/IterList.v new file mode 100644 index 00000000..49beb1c5 --- /dev/null +++ b/lib/IterList.v @@ -0,0 +1,96 @@ +Require Import Coqlib. + +(** TODO: are these def and lemma already defined in the standard library ? + +In this case, it should be better to reuse those of the standard library ! + +*) + +Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A := + match n with + | O => x + | S n0 => iter n0 f (f x) + end. + +Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x). +Proof. + induction n; simpl; auto. + intros; erewrite <- IHn; simpl; auto. +Qed. + +Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x). +Proof. + induction n; simpl; auto. +Qed. + +Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l. + +Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l). +Proof. + apply iter_S. +Qed. + +Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l). +Proof. + apply iter_plus. +Qed. + +Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2. +Proof. + induction l1; auto. +Qed. + +Lemma iter_tail_nil A n: @iter_tail A n nil = nil. +Proof. + unfold iter_tail; induction n; simpl; auto. +Qed. + +Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil. +Proof. + rewrite (app_nil_end l) at 2. + rewrite iter_tail_length. + auto. +Qed. + +Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat. +Proof. + unfold iter_tail; induction n; auto. + intros l; destruct l. { simpl; omega. } + intros; simpl. erewrite IHn; eauto. + simpl in *; omega. +Qed. + +Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l). +Proof. + unfold iter_tail; induction n; simpl. + - intros l; destruct l; simpl; omega || eauto. + - intros l H; destruct (IHn (tl l)) as (x & H1). + + destruct l; simpl in *; try omega. + + rewrite H1; eauto. +Qed. + +Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2. +Proof. + intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto. + rewrite EQ. + rewrite (length_iter_tail n2 l); eauto. + omega. +Qed. + +Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat. +Proof. + destruct (le_lt_dec n (List.length l)); try omega. + intros; exploit (iter_tail_inject1 n (length l) l); try omega. + rewrite iter_tail_reach_nil. auto. +Qed. + +Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l). +Proof. + induction l; auto. + rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega. +Qed. + +Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l). +Proof. + intros; rewrite list_length_z_nat, Nat2Z.id. auto. +Qed. diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v new file mode 100644 index 00000000..824a9c2f --- /dev/null +++ b/lib/OptionMonad.v @@ -0,0 +1,49 @@ +(* Declare Scope option_monad_scope. *) + +Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end) + (at level 200, X ident, A at level 100, B at level 200) + : option_monad_scope. + +Notation "'ASSERT' A 'IN' B" := (if A then B else None) + (at level 200, A at level 100, B at level 200) + : option_monad_scope. + +Local Open Scope option_monad_scope. + + +(** Simple tactics for option-monad *) + +Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B): + (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B): + (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Ltac inversion_SOME x := + try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]). + +Ltac inversion_ASSERT := + try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]). + +Ltac simplify_someHyp := + match goal with + | H: None = Some _ |- _ => inversion H; clear H; subst + | H: Some _ = None |- _ => inversion H; clear H; subst + | H: ?t = ?t |- _ => clear H + | H: Some _ = Some _ |- _ => inversion H; clear H; subst + | H: Some _ <> None |- _ => clear H + | H: None <> Some _ |- _ => clear H + | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H + end. + +Ltac simplify_someHyps := + repeat (simplify_someHyp; simpl in * |- *). + +Ltac try_simplify_someHyps := + try (intros; simplify_someHyps; eauto). |