aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Util/FixedWordSizesEquality.v102
-rw-r--r--src/Util/NatUtil.v26
-rw-r--r--src/Util/WordUtil.v51
3 files changed, 178 insertions, 1 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
new file mode 100644
index 000000000..7ac993871
--- /dev/null
+++ b/src/Util/FixedWordSizesEquality.v
@@ -0,0 +1,102 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.NArith.BinNat.
+Require Import Coq.Arith.Arith.
+Require Import Bedrock.Word.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Util.WordUtil.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+Definition wordT_beq_hetero {logsz1 logsz2} : wordT logsz1 -> wordT logsz2 -> bool
+ := match logsz1 return wordT logsz1 -> wordT logsz2 -> bool with
+ | 5 as logsz1' | 6 as logsz1' | 7 as logsz1'
+ | _ as logsz1'
+ => match logsz2 return wordT logsz1' -> wordT logsz2 -> bool with
+ | 5 as logsz2' | 6 as logsz2' | 7 as logsz2'
+ | _ as logsz2'
+ => @Word.weqb_hetero (2^logsz1') (2^logsz2')
+ end
+ end.
+
+(* transparent so the equality proof can compute away *)
+Lemma pow2_inj_helper x y : 2^x = 2^y -> x = y.
+Proof.
+ destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ].
+ intro H; exfalso.
+ abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; omega).
+Defined.
+Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl.
+Proof.
+ induction x; simpl; [ reflexivity | ].
+ etransitivity; [ | exact (f_equal (fun p => f_equal S p) (IHx eq_refl)) ]; clear IHx.
+ unfold pow2_inj_helper in *; simpl.
+ pose proof (NatUtil.nat_eq_dec_S x x).
+ do 2 edestruct NatUtil.nat_eq_dec; try assumption; try (exfalso; assumption).
+ match goal with
+ | [ H : ?x <> ?x |- _ ] => exfalso; clear -H; exact (H eq_refl)
+ end.
+Defined.
+Lemma pow2_inj_helper_eq_rect x y P v v'
+ : (exists pf : 2^x = 2^y, eq_rect _ P v _ pf = v')
+ -> (exists pf : x = y, eq_rect _ (fun e => P (2^e)) v _ pf = v').
+Proof.
+ intros [pf H]; exists (pow2_inj_helper x y pf); subst v'.
+ destruct (NatUtil.nat_eq_dec x y) as [H|H];
+ [ | exfalso; clear -pf H;
+ abstract (apply pow2_inj_helper in pf; omega) ].
+ subst; rewrite pow2_inj_helper_refl; simpl.
+ pose proof (NatUtil.UIP_nat_transparent _ _ pf eq_refl); subst pf.
+ reflexivity.
+Defined.
+
+Definition wordT_beq_lb logsz1
+ : forall x y : wordT logsz1, x = y -> wordT_beq_hetero x y = true
+ := match logsz1 return forall x y : wordT logsz1, x = y -> wordT_beq_hetero x y = true with
+ | 5 as logsz1' | 6 as logsz1' | 7 as logsz1'
+ | _ as logsz1'
+ => fun x y pf => proj2 (@Word.weqb_hetero_true_iff (2^logsz1') x (2^logsz1') y) (ex_intro _ eq_refl pf)
+ end.
+Definition wordT_beq_hetero_lb {logsz1 logsz2}
+ : forall x y, (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y) -> wordT_beq_hetero x y = true.
+Proof.
+ intros x y [pf H]; subst logsz2; revert x y H; simpl.
+ apply wordT_beq_lb.
+Defined.
+
+Definition wordT_beq_bl logsz
+ : forall x y : wordT logsz, wordT_beq_hetero x y = true -> x = y
+ := match logsz return forall x y : wordT logsz, wordT_beq_hetero x y = true -> x = y with
+ | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7
+ | _
+ => fun x y pf => proj1 (Word.weqb_hetero_homo_true_iff _ x y) pf
+ end.
+
+Lemma wordT_beq_hetero_type_lb_false logsz1 logsz2 x y : logsz1 <> logsz2 -> @wordT_beq_hetero logsz1 logsz2 x y = false.
+Proof.
+ destruct (wordT_beq_hetero x y) eqn:H; [ | reflexivity ].
+ revert H.
+ repeat (try destruct logsz1 as [|logsz1];
+ try destruct logsz2 as [|logsz2];
+ try (intros; omega);
+ try (intro H'; apply Word.weqb_hetero_true_iff in H'; destruct H' as [pf H']; pose proof (pow2_inj_helper _ _ pf); try omega)).
+Qed.
+
+Definition wordT_beq_hetero_bl {logsz1 logsz2}
+ : forall x y, wordT_beq_hetero x y = true -> (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y).
+Proof.
+ refine match logsz1, logsz2 return forall x y, wordT_beq_hetero x y = true -> (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y) with
+ | 0, 0 | 1, 1 | 2, 2 | 3, 3 | 4, 4 | 5, 5 | 6, 6
+ | 7, 7
+ => fun x y pf => ex_intro _ eq_refl (@wordT_beq_bl _ x y pf)
+ | S (S (S (S (S (S (S (S a))))))), S (S (S (S (S (S (S (S b)))))))
+ => match NatUtil.nat_eq_dec a b with
+ | left pf
+ => match pf with
+ | eq_refl => fun x y pf => ex_intro _ eq_refl (@wordT_beq_bl _ x y pf)
+ end
+ | right n => fun x y pf => match _ : False with end
+ end
+ | _, _
+ => fun x y pf => match _ : False with end
+ end;
+ try abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence).
+Defined.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index fd2102b23..99d0be29c 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -59,6 +59,32 @@ Tactic Notation "omega" := coq_omega.
Tactic Notation "omega" "*" := omega_with_min_max_case.
Tactic Notation "omega" "**" := omega_with_min_max.
+Lemma nat_eq_dec_S x y
+ : match nat_eq_dec (S x) (S y), nat_eq_dec x y with
+ | left pfS, left pf => pfS = f_equal S pf
+ | right _, right _ => True
+ | _, _ => False
+ end.
+Proof.
+ unfold nat_eq_dec; simpl.
+ match goal with
+ | [ |- match match ?e with _ => _ end with _ => _ end ]
+ => destruct e
+ end; simpl; try exact I.
+ reflexivity.
+Defined.
+
+Lemma UIP_nat_transparent x y (p1 p2 : x = y :> nat) : p1 = p2.
+Proof.
+ transitivity (match nat_eq_dec x y, nat_eq_dec y y with
+ | left pf1, left pf2 => eq_trans pf1 (eq_sym pf2)
+ | _, _ => p1
+ end);
+ [ revert p2 | revert p1 ];
+ subst y; intro p;
+ destruct (nat_eq_dec x x) as [q|q]; case q; reflexivity.
+Defined.
+
Lemma nat_beq_false_iff x y : nat_beq x y = false <-> x <> y.
Proof.
split; intro H; repeat intro; subst.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 7f8d7b824..bd00e1c33 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -10,10 +10,13 @@ Require Import Coq.Bool.Bool.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.NatUtil.
Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Sigma.
Require Import Bedrock.Word.
Require Import Bedrock.Nomega.
+Require Import Crypto.Util.FixCoqMistakes.
+
Local Open Scope nat_scope.
Create HintDb pull_wordToN discriminated.
@@ -51,7 +54,53 @@ Module Word.
| [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
=> apply IHx
end ].
- Qed.
+ Defined.
+ (* oh, the hoops I jump through to make this transparent... *)
+ Theorem weqb_hetero_homo_true_iff : forall sz x y,
+ @weqb_hetero sz sz x y = true <-> x = y.
+ Proof.
+ etransitivity; [ apply weqb_hetero_true_iff | ].
+ split; [ intros [pf H] | intro ]; try (subst y; exists eq_refl; reflexivity).
+ revert y H; induction x as [|b n x IHx]; intros.
+ { subst y;
+ refine match pf in (_ = z)
+ return match z return 0 = z -> Prop with
+ | 0 => fun pf => WO = eq_rect 0 word WO 0 pf
+ | _ => fun pf => True
+ end pf
+ with
+ | eq_refl => eq_refl
+ end. }
+ { revert x y H IHx.
+ refine (match pf in _ = Sn
+ return match Sn return S n = Sn -> Prop with
+ | 0 => fun _ => True
+ | S n' => fun pf =>
+ forall (pfn : n = n')
+ (x : word n)
+ (y : word (S n'))
+ (H : eq_rect (S n) word (WS b x) (S n') pf = y)
+ (IHx : forall (pf : n = n') (y : word n'), eq_rect n word x n' pf = y -> eq_rect n word x n' pfn = y),
+ WS b (eq_rect n word x n' pfn) = y
+ end pf
+ with
+ | eq_refl
+ => fun pfn x y H IHx
+ => eq_trans
+ (f_equal2 (fun b => @WS b _)
+ (f_equal (@whd _) H)
+ (IHx eq_refl (wtl y) (f_equal (@wtl _) H)))
+ _
+ end eq_refl).
+ refine match y in word Sn return match Sn return word Sn -> Prop with
+ | 0 => fun _ => True
+ | S n => fun y => WS (whd y) (wtl y) = y
+ end y
+ with
+ | WS _ _ _ => eq_refl
+ | _ => I
+ end. }
+ Defined.
End Word.
(* Utility Tactics *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:01:08 +0000