aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/CommonSubexpressionEliminationProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/CommonSubexpressionEliminationProperties.v')
-rw-r--r--src/Compilers/CommonSubexpressionEliminationProperties.v189
1 files changed, 0 insertions, 189 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationProperties.v b/src/Compilers/CommonSubexpressionEliminationProperties.v
deleted file mode 100644
index b52afcb18..000000000
--- a/src/Compilers/CommonSubexpressionEliminationProperties.v
+++ /dev/null
@@ -1,189 +0,0 @@
-(** * Common Subexpression Elimination for PHOAS Syntax *)
-Require Import Coq.omega.Omega.
-Require Import Coq.Lists.List.
-Require Import Coq.FSets.FMapInterface.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Equality.
-Require Import Crypto.Compilers.CommonSubexpressionElimination.
-Require Import Crypto.Util.NatUtil.
-
-Local Open Scope list_scope.
-
-Local Open Scope ctype_scope.
-Section symbolic.
- (** Holds decidably-equal versions of raw expressions, for lookup. *)
- Context (base_type_code : Type)
- (op_code : Type)
- (base_type_code_beq : base_type_code -> base_type_code -> bool)
- (op_code_beq : op_code -> op_code -> bool)
- (base_type_code_bl : forall x y, base_type_code_beq x y = true -> x = y)
- (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true)
- (op_code_bl : forall x y, op_code_beq x y = true -> x = y)
- (op_code_lb : forall x y, x = y -> op_code_beq x y = true)
- (op : flat_type base_type_code -> flat_type base_type_code -> Type)
- (symbolize_op : forall s d, op s d -> op_code)
- (op_code_leb : op_code -> op_code -> bool)
- (base_type_leb : base_type_code -> base_type_code -> bool)
- (op_code_leb_total : forall x y, op_code_leb x y = true \/ op_code_leb y x = true)
- (base_type_leb_total : forall x y, base_type_leb x y = true \/ base_type_leb y x = true)
- (op_code_leb_antisymmetric : forall x y, op_code_leb x y = true -> op_code_leb y x = true -> op_code_beq x y = true)
- (base_type_leb_antisymmetric : forall x y, base_type_leb x y = true -> base_type_leb y x = true -> base_type_code_beq x y = true).
- Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
- Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr).
-
- Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code op_code base_type_code_beq op_code_beq).
- Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code op_code base_type_code_beq op_code_beq base_type_code_lb op_code_lb).
- Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
-
- Local Notation flat_type := (flat_type base_type_code).
- Local Notation type := (type base_type_code).
- Local Notation exprf := (@exprf base_type_code op).
- Local Notation expr := (@expr base_type_code op).
- Local Notation Expr := (@Expr base_type_code op).
-
- Local Notation symbolic_expr_leb := (@symbolic_expr_leb base_type_code op_code base_type_code_beq op_code_beq op_code_leb base_type_leb).
- Local Notation flat_type_leb := (@flat_type_leb base_type_code base_type_code_beq base_type_leb).
- Local Notation flat_type_beq := (@flat_type_beq base_type_code base_type_code_beq).
- Local Notation flat_type_bl := (@internal_flat_type_dec_bl base_type_code base_type_code_beq base_type_code_bl).
- Local Notation flat_type_lb := (@internal_flat_type_dec_lb base_type_code base_type_code_beq base_type_code_lb).
-
- Lemma base_type_leb_reflexive x : base_type_leb x x = true.
- Proof using base_type_leb_total. destruct (base_type_leb_total x x); assumption. Qed.
-
- Lemma op_code_leb_reflexive x : op_code_leb x x = true.
- Proof using op_code_leb_total. destruct (op_code_leb_total x x); assumption. Qed.
-
- Theorem flat_type_leb_total : forall a1 a2, flat_type_leb a1 a2 = true \/ flat_type_leb a2 a1 = true.
- Proof using base_type_code_bl base_type_leb_total.
- induction a1, a2;
- repeat first [ progress simpl
- | progress subst
- | solve [ auto ]
- | match goal with
- | [ H : forall a2', ?leb ?a1 a2' = true \/ _ |- context[?leb ?a1 ?a2] ]
- => let H' := fresh in destruct (H a2) as [H'|H']; rewrite H'
- | [ H : flat_type_beq _ _ = true |- _ ] => apply flat_type_bl in H
- | [ |- context[flat_type_beq ?x ?y] ]
- => destruct (flat_type_beq x y) eqn:?
- end ].
- Qed.
-
- Theorem flat_type_leb_reflexive x : flat_type_leb x x = true.
- Proof using base_type_code_bl base_type_leb_total. destruct (flat_type_leb_total x x); assumption. Qed.
-
- Local Ltac rewrite_beq_leb_flat_type_op_code_reflexive :=
- repeat match goal with
- | [ H : flat_type_beq _ _ = true |- _ ] => apply flat_type_bl in H
- | [ H : op_code_beq _ _ = true |- _ ] => apply op_code_bl in H
- | [ H : symbolic_expr_beq _ _ = true |- _ ] => apply symbolic_expr_bl in H
- | [ H : context[flat_type_leb ?x ?x] |- _ ]
- => rewrite (flat_type_leb_reflexive x) in H
- | [ |- context[flat_type_leb ?x ?x] ]
- => rewrite (flat_type_leb_reflexive x)
- | [ H : context[flat_type_beq ?x ?x] |- _ ]
- => rewrite (flat_type_lb x x eq_refl) in H
- | [ |- context[flat_type_beq ?x ?x] ]
- => rewrite (flat_type_lb x x eq_refl)
- | [ H : context[op_code_leb ?x ?x] |- _ ]
- => rewrite (op_code_leb_reflexive x) in H
- | [ |- context[op_code_leb ?x ?x] ]
- => rewrite (op_code_leb_reflexive x)
- | [ H : context[op_code_beq ?x ?x] |- _ ]
- => rewrite (op_code_lb x x eq_refl) in H
- | [ |- context[op_code_beq ?x ?x] ]
- => rewrite (op_code_lb x x eq_refl)
- end.
-
- Theorem flat_type_leb_antisymmetric : forall a1 a2, flat_type_leb a1 a2 = true -> flat_type_leb a2 a1 = true -> flat_type_beq a1 a2 = true.
- Proof using base_type_code_bl base_type_code_lb base_type_leb_antisymmetric base_type_leb_total.
- induction a1, a2;
- repeat first [ progress simpl
- | progress subst
- | solve [ auto ]
- | progress rewrite ?andb_true_r, ?orb_false_r
- | progress rewrite_beq_leb_flat_type_op_code_reflexive
- | match goal with
- | [ |- context[flat_type_beq ?x ?y] ]
- => destruct (flat_type_beq x y) eqn:?
- | [ H : forall a2, ?leb ?x a2 = true -> ?leb a2 ?x = true -> _, H0 : ?leb ?x ?a2' = true, H1 : ?leb ?a2' ?x = true |- _ ]
- => specialize (H _ H0 H1)
- end
- | progress intros ].
- Qed.
-
- Theorem symbolic_expr_leb_total : forall a1 a2, symbolic_expr_leb a1 a2 = true \/ symbolic_expr_leb a2 a1 = true.
- Proof using base_type_code_bl base_type_code_lb base_type_leb_total op_code_bl op_code_lb op_code_leb_total.
- induction a1, a2;
- repeat first [ rewrite !PeanoNat.Nat.leb_le
- | progress subst
- | progress simpl
- | solve [ auto ]
- | omega
- | progress rewrite_beq_leb_flat_type_op_code_reflexive
- | match goal with
- | [ |- context[flat_type_beq ?x ?y] ]
- => destruct (flat_type_beq x y) eqn:?
- | [ |- context[op_code_beq ?x ?y] ]
- => destruct (op_code_beq x y) eqn:?
- | [ |- context[symbolic_expr_beq ?x ?y] ]
- => destruct (symbolic_expr_beq x y) eqn:?
- | [ H : forall a2', ?leb ?a1 a2' = true \/ _ |- context[?leb ?a1 ?a2] ]
- => let H' := fresh in destruct (H a2) as [H'|H']; rewrite H'
- | [ |- context[flat_type_leb ?a1 ?a2] ]
- => let H' := fresh in destruct (flat_type_leb_total a1 a2) as [H'|H']; rewrite H'
- | [ |- context[op_code_leb ?a1 ?a2] ]
- => let H' := fresh in destruct (op_code_leb_total a1 a2) as [H'|H']; rewrite H'
- end ].
- Qed.
-
- Theorem symbolic_expr_leb_reflexive x : symbolic_expr_leb x x = true.
- Proof using base_type_code_bl base_type_code_lb base_type_leb_total op_code_bl op_code_lb op_code_leb_total. destruct (symbolic_expr_leb_total x x); assumption. Qed.
-
- Local Ltac rewrite_beq_leb_symbolic_expr_reflexive :=
- repeat match goal with
- | [ H : symbolic_expr_beq _ _ = true |- _ ] => apply symbolic_expr_bl in H
- | [ H : context[symbolic_expr_leb ?x ?x] |- _ ]
- => rewrite (symbolic_expr_leb_reflexive x) in H
- | [ |- context[symbolic_expr_leb ?x ?x] ]
- => rewrite (symbolic_expr_leb_reflexive x)
- | [ H : context[symbolic_expr_beq ?x ?x] |- _ ]
- => rewrite (symbolic_expr_lb x x eq_refl) in H
- | [ |- context[symbolic_expr_beq ?x ?x] ]
- => rewrite (symbolic_expr_lb x x eq_refl)
- end.
-
- Theorem symbolic_expr_leb_antisymmetric : forall a1 a2, symbolic_expr_leb a1 a2 = true -> symbolic_expr_leb a2 a1 = true -> symbolic_expr_beq a1 a2 = true.
- Proof using base_type_code_bl base_type_code_lb base_type_leb_antisymmetric base_type_leb_total op_code_bl op_code_lb op_code_leb_antisymmetric op_code_leb_total.
- induction a1, a2;
- repeat first [ rewrite !PeanoNat.Nat.leb_le
- | progress subst
- | progress simpl
- | solve [ auto ]
- | omega
- | progress rewrite ?andb_true_r, ?orb_false_r
- | progress rewrite_beq_leb_flat_type_op_code_reflexive
- | progress rewrite_beq_leb_symbolic_expr_reflexive
- | match goal with
- | [ |- context[flat_type_beq ?x ?y] ]
- => destruct (flat_type_beq x y) eqn:?
- | [ |- context[op_code_beq ?x ?y] ]
- => destruct (op_code_beq x y) eqn:?
- | [ |- context[symbolic_expr_beq ?x ?y] ]
- => destruct (symbolic_expr_beq x y) eqn:?
- | [ |- context[nat_beq ?x ?x] ]
- => rewrite (internal_nat_dec_lb x x eq_refl)
- | [ |- context[flat_type_leb ?a1 ?a2] ]
- => let H' := fresh in destruct (flat_type_leb_total a1 a2) as [H'|H']; rewrite H'
- | [ |- context[op_code_leb ?a1 ?a2] ]
- => let H' := fresh in destruct (op_code_leb_total a1 a2) as [H'|H']; rewrite H'
- | [ H : ?x <= ?y, H' : ?y <= ?x |- _ ] => assert (x = y) by omega; clear H H'
- | [ H : forall a2, ?leb ?x a2 = true -> ?leb a2 ?x = true -> _, H0 : ?leb ?x ?a2' = true, H1 : ?leb ?a2' ?x = true |- _ ]
- => specialize (H _ H0 H1)
- | [ H0 : flat_type_leb ?x' ?y' = true, H1 : flat_type_leb ?y' ?x' = true |- _ ]
- => pose proof (flat_type_leb_antisymmetric _ _ H0 H1); clear H0 H1
- | [ H : forall x y, ?leb x y = true -> ?leb y x = true -> _, H0 : ?leb ?x' ?y' = true, H1 : ?leb ?y' ?x' = true |- _ ]
- => pose proof (H _ _ H0 H1); clear H0 H1
- end
- | progress intros ].
- Qed.
-End symbolic.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 07:23:46 +0000