Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass

1 files changed, 49 insertions, 0 deletions

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).