moved generic stuff from squiggleeq: fwd tactics and decision helpers

_CoqProject

@@ -7,6 +7,7 @@ theories/Core/Any.v
 theories/Core/CmpDec.v
 theories/Core/EquivDec.v
 theories/Core/RelDec.v
+theories/Core/Decision.v
 
 theories/Structures/Applicative.v
 theories/Structures/BinOps.v
@@ -101,6 +102,7 @@ theories/Tactics/Injection.v
 theories/Tactics/MonadTac.v
 theories/Tactics/Parametric.v
 theories/Tactics/Reify.v
+theories/Tactics/Hide.v
 
 theories/Data/Graph/BuildGraph.v
 theories/Data/Graph/GraphAdjList.v

theories/Core/Decision.v

@@ -0,0 +1,23 @@
+Require Import Coq.Classes.DecidableClass.
+
+Definition decideP (P : Prop) (D : Decidable P) : {P} + {~P} :=
+  match @Decidable_witness P D as X return (X = true -> P) -> (X = false -> ~P) -> {P} + {~P} with
+  | true => fun pf _ => left (pf eq_refl)
+  | false => fun _ pf => right (pf eq_refl)
+  end (@Decidable_sound _ D) (@Decidable_complete_alt _ D).
+
+Ltac cases_ifd Hn :=
+  match goal with
+    |- context[if ?d then ?tt else ?ff] =>
+    let Hnt := fresh Hn "t" in
+    let Hnf := fresh Hn "f" in
+    destruct d as [Hnt | Hnf] end.
+
+Lemma decide_decideP  {P:Prop }`{Decidable P} {R:Type} (a b : R) :
+  (if (decide P) then  a else b) = (if (decideP P) then  a else b).
+Proof.
+  symmetry. unfold decide.
+  destruct (decideP P).
+- rewrite Decidable_complete; auto.
+- rewrite Decidable_sound_alt; auto.
+Qed.

theories/Tactics/Forward.v

@@ -16,3 +16,34 @@ Ltac forward_reason :=
                clear H'
              end
          end.
+
+Ltac rwHyps :=
+  repeat match goal with
+           [ H: _ = _ |- _] =>  rewrite -> H
+         end.
+
+Ltac rwHypsR :=
+  repeat match goal with
+           [ H: _ = _ |- _] =>  rewrite <- H
+         end.
+
+Ltac rwHypsA :=
+  repeat match goal with
+           [ H: _ = _ |- _] =>  rewrite -> H in *
+         end.
+
+Ltac rwHypsRA :=
+  repeat match goal with
+           [ H: _ = _ |- _] =>  rewrite <- H in *
+         end.
+
+(* based on a tactic written by Vincent Rahli *)
+Ltac clear_trivials :=
+  repeat match goal with
+           | [ H : ?T = ?T |- _ ] => clear H
+           | [ H : ?T <-> ?T |- _ ] => clear H
+           | [ H : ?T -> ?T |- _ ] => clear H
+           | [ H1 : ?T, H2 : ?T |- _ ] => clear H2
+           | [ H : True |- _ ] => clear H
+           | [ H : not False |- _ ] => clear H
+         end.

theories/Tactics/Hide.v

@@ -0,0 +1,22 @@
+(* The names of the tactics here come from the 2013 distribution 
+of Software Foundations (SF). The implementations are different, though:
+1) The hiding mechanism is SF was not fully reliable:
+ tactics that compute on hypotheses could unhide stuff
+2) Hiding in SF was always reversible. Here, unhiding only works
+when proving a Prop. We can change
+the return type to [Type]. But then hiding hypothesis can make
+things unprovable by introducing universe constraints.
+*)
+
+Inductive Hidden (P:Type) : Prop:=
+| hidden (p:P): Hidden P.
+
+Ltac show_hyp H :=
+  destruct H as [H].
+
+Ltac hide_hyp H :=
+  apply hidden in H.
+
+Ltac show_hyps :=
+  repeat match goal with
+           H: Hidden _ |- _ => show_hyp H end.