Add trueify to src/Util/PartiallyReifiedProp.v

1 files changed, 19 insertions, 7 deletions

diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v
index d85473271..c950b0971 100644
--- a/src/Util/PartiallyReifiedProp.v
+++ b/src/Util/PartiallyReifiedProp.v
@@ -7,7 +7,7 @@ Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.
 
 Delimit Scope reified_prop_scope with reified_prop.
-Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | rEqRefl {T} (x : T) | inject (_ : Prop).
+Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | inject (_ : Prop).
 Bind Scope reified_prop_scope with reified_Prop.
 
 Fixpoint to_prop (x : reified_Prop) : Prop
@@ -19,7 +19,6 @@ Fixpoint to_prop (x : reified_Prop) : Prop
      | rImpl x y => to_prop x -> to_prop y
      | @rForall _ f => forall x, to_prop (f x)
      | @rEq _ x y => x = y
-     | @rEqRefl _ x => x = x
      | inject x => x
      end.
 
@@ -82,10 +81,6 @@ Definition reified_Prop_eq (x y : reified_Prop)
                       eq_rect _ (fun t => t) x0 _ pf = y0
                       /\ eq_rect _ (fun t => t) x1 _ pf = y1
      | rEq _ _ _, _ => False
-     | @rEqRefl Tx x, @rEqRefl Ty y
-       => exists pf : Tx = Ty,
-                      eq_rect _ (fun t => t) x _ pf = y
-     | rEqRefl _ _, _ => False
      | inject x, inject y => x = y
      | inject _, _ => False
      end.
@@ -138,7 +133,6 @@ Ltac inversion_reified_Prop_step :=
   | [ H : rImpl _ _ = _ |- _ ] => do_on H
   | [ H : rForall _ = _ |- _ ] => do_on H
   | [ H : rEq _ _ = _ |- _ ] => do_on H
-  | [ H : rEqRefl _ = _ |- _ ] => do_on H
   | [ H : inject _ = _ |- _ ] => do_on H
   end.
 Ltac inversion_reified_Prop := repeat inversion_reified_Prop_step.
@@ -148,3 +142,21 @@ Proof.
   destruct x, y; simpl; try tauto.
   { split; intro H; inversion H; subst; repeat split. }
 Qed.
+
+(** Remove all possibly false terms in a reified prop *)
+Fixpoint trueify (p : reified_Prop) : reified_Prop
+  := match p with
+     | rTrue => rTrue
+     | rFalse => rTrue
+     | rAnd x y => rAnd (trueify x) (trueify y)
+     | rOr x y => rOr (trueify x) (trueify y)
+     | rImpl x y => rImpl x (trueify y)
+     | rForall T f => rForall (fun x => trueify (f x))
+     | rEq T x y => rEq x x
+     | inject x => inject True
+     end.
+
+Lemma trueify_true : forall p, to_prop (trueify p).
+Proof.
+  induction p; simpl; auto.
+Qed.