From 52a84764eadd3e673869c2cd1d868a7809e55871 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 6 Nov 2017 12:38:24 -0500 Subject: Update versions of id_with_alt_cps These type signatures allow better reification --- src/Util/CPSUtil.v | 167 ++++++++++++++++++++++++++--------------------------- 1 file changed, 83 insertions(+), 84 deletions(-) (limited to 'src/Util/CPSUtil.v') diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index 58284ad88..bb36cc519 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -4,6 +4,7 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.LetIn. Require Crypto.Util.Tuple. Local Notation tuple := Tuple.tuple. Local Open Scope Z_scope. @@ -13,98 +14,96 @@ Create HintDb uncps discriminated. Lemma push_id {A} (a:A) : id a = a. reflexivity. Qed. Hint Rewrite @push_id : push_id. -Definition id_with_alt_cps {R A} (value : A) (value_for_alt : A) (f : A -> R) : R - := f (id_with_alt value value_for_alt). +Definition id_with_alt_cps' {R A} (value value_for_alt : (A -> A) -> A) (f : A -> R) : R + := dlet z := id_with_alt (value id) (value_for_alt id) in + f z. +Definition id_with_alt_cps {R A} (value value_for_alt : (A -> R) -> R) (f : A -> R) : R + := id_with_alt (value f) (value_for_alt f). +Definition id_with_alt_cps'_correct {R A} value value_for_alt f + : @id_with_alt_cps' R A value value_for_alt f = f (id_with_alt (value id) (value_for_alt id)) + := eq_refl. +Hint Rewrite @id_with_alt_cps'_correct : uncps. Definition id_with_alt_cps_correct {R A} value value_for_alt f - : @id_with_alt_cps R A value value_for_alt f = f (id_with_alt value value_for_alt) + : @id_with_alt_cps R A value value_for_alt f = id_with_alt (value f) (value_for_alt f) := eq_refl. Hint Rewrite @id_with_alt_cps_correct : uncps. +Definition id_with_alt_cps'_correct_gen {R A} (value value_for_alt : forall R, (A -> R) -> R) f + : @id_with_alt_cps' R A (value _) (value_for_alt _) f = f (id_with_alt (value _ id) (value_for_alt _ id)) + := eq_refl. +Hint Rewrite @id_with_alt_cps'_correct_gen : uncps. +Definition id_with_alt_cps_correct_gen {R A} (value value_for_alt : forall R, (A -> R) -> R) f + (Hvalue : value _ f = f (value _ id)) + : @id_with_alt_cps R A (value _) (value_for_alt _) f = f (id_with_alt (value _ id) (value_for_alt _ id)). +Proof. + cbv [id_with_alt_cps id_with_alt]; assumption. +Defined. +Hint Rewrite @id_with_alt_cps_correct_gen : uncps. + +Definition id_tuple'_with_alt_cps' {R A n} + (value value_for_alt : (Tuple.tuple' A n -> Tuple.tuple' A n) -> Tuple.tuple' A n) + (f : Tuple.tuple' A n -> R) + : R + := dlet z := id_tuple'_with_alt (value id) (value_for_alt id) in + f z. +Definition id_tuple_with_alt_cps' {R A n} + (value value_for_alt : (Tuple.tuple A n -> Tuple.tuple A n) -> Tuple.tuple A n) + (f : Tuple.tuple A n -> R) + : R + := dlet z := id_tuple_with_alt (value id) (value_for_alt id) in + f z. -Definition id_with_alt_proof_cps {R A} (value : A) (value_for_alt : A) - {pf : value = value_for_alt} (f : A -> R) +Definition id_tuple'_with_alt_cps'_correct {R A n} value value_for_alt f + : @id_tuple'_with_alt_cps' R A n value value_for_alt f = f (id_tuple'_with_alt (value id) (value_for_alt id)) + := eq_refl. +Hint Rewrite @id_tuple'_with_alt_cps'_correct : uncps. + +Definition id_tuple_with_alt_cps'_correct {R A n} value value_for_alt f + : @id_tuple_with_alt_cps' R A n value value_for_alt f = f (id_tuple_with_alt (value id) (value_for_alt id)) + := eq_refl. +Hint Rewrite @id_tuple_with_alt_cps'_correct : uncps. + +Definition id_tuple'_with_alt_cps {R A n} + (value value_for_alt : (Tuple.tuple' A n -> R) -> R) + (f : Tuple.tuple' A n -> R) + : R + := id_with_alt (value f) (value_for_alt f). +Definition id_tuple_with_alt_cps {R A n} + (value value_for_alt : (Tuple.tuple A n -> R) -> R) + (f : Tuple.tuple A n -> R) : R - := id_with_alt_cps value value_for_alt f. -Definition id_with_alt_proof_cps_correct {R A} value value_for_alt pf f - : @id_with_alt_proof_cps R A value value_for_alt pf f = f (@id_with_alt_proof A value value_for_alt pf) + := id_with_alt (value f) (value_for_alt f). + +Definition id_tuple'_with_alt_cps_correct {R A n} value value_for_alt f + : @id_tuple'_with_alt_cps R A n value value_for_alt f = id_with_alt (value f) (value_for_alt f) := eq_refl. -Hint Rewrite @id_with_alt_proof_cps_correct : uncps. - -Section id_tuple_with_alt. - Context {R A : Type}. - - Fixpoint id_tuple'_with_alt_cps {n} - {struct n} - : forall (value value_for_alt : Tuple.tuple' A n), - (Tuple.tuple' A n -> R) - -> R - := match n return forall value value_for_alt : Tuple.tuple' A n, (Tuple.tuple' A n -> R) -> R with - | O => id_with_alt_cps - | S n' => fun (value value_for_alt : Tuple.tuple' A n' * A) (f : Tuple.tuple' A n' * A -> R) - => @id_tuple'_with_alt_cps - n' (fst value) (fst value_for_alt) - (fun ts - => @id_with_alt_cps - R A (snd value) (snd value_for_alt) - (fun t => f (ts, t))) - end. - Fixpoint id_tuple'_with_alt_proof_cps {n} - {struct n} - : forall (value value_for_alt : Tuple.tuple' A n) {pf : value = value_for_alt}, - (Tuple.tuple' A n -> R) - -> R - := match n return forall value value_for_alt : Tuple.tuple' A n, _ -> (Tuple.tuple' A n -> R) -> R with - | O => id_with_alt_proof_cps - | S n' => fun (value value_for_alt : Tuple.tuple' A n' * A) (pf : value = value_for_alt) - (f : Tuple.tuple' A n' * A -> R) - => @id_tuple'_with_alt_proof_cps - n' (fst value) (fst value_for_alt) - (f_equal (@fst _ _) pf) - (fun ts - => @id_with_alt_proof_cps - R A (snd value) (snd value_for_alt) - (f_equal (@snd _ _) pf) - (fun t => f (ts, t))) - end. - Definition id_tuple_with_alt_cps {n} - : forall (value value_for_alt : Tuple.tuple A n), (Tuple.tuple A n -> R) -> R - := match n with - | O => id_with_alt_cps - | S n' => id_tuple'_with_alt_cps - end. - Definition id_tuple_with_alt_proof_cps {n} - : forall (value value_for_alt : Tuple.tuple A n) {pf : value = value_for_alt}, - (Tuple.tuple A n -> R) -> R - := match n with - | O => id_with_alt_proof_cps - | S n' => id_tuple'_with_alt_proof_cps - end. -End id_tuple_with_alt. - -Local Ltac t_ind n := - let IHn := fresh "IHn" in - induction n as [|n IHn]; cbn [id_tuple'_with_alt_cps id_tuple'_with_alt_proof_cps id_tuple'_with_alt id_tuple'_with_alt_proof]; - [ reflexivity - | rewrite IHn; try reflexivity ]. -Lemma id_tuple'_with_alt_cps_correct {R A n} value value_for_alt f - : @id_tuple'_with_alt_cps R A n value value_for_alt f - = f (@id_tuple'_with_alt A n value value_for_alt). -Proof. t_ind n. Qed. Hint Rewrite @id_tuple'_with_alt_cps_correct : uncps. -Lemma id_tuple'_with_alt_proof_cps_correct {R A n} value value_for_alt pf f - : @id_tuple'_with_alt_proof_cps R A n value value_for_alt pf f - = f (@id_tuple'_with_alt_proof A n value value_for_alt pf). -Proof. t_ind n. Qed. -Hint Rewrite @id_tuple'_with_alt_proof_cps_correct : uncps. -Lemma id_tuple_with_alt_cps_correct {R A n} value value_for_alt f - : @id_tuple_with_alt_cps R A n value value_for_alt f - = f (@id_tuple_with_alt A n value value_for_alt). -Proof. destruct n; [ reflexivity | apply id_tuple'_with_alt_cps_correct ]. Qed. + +Definition id_tuple_with_alt_cps_correct {R A n} value value_for_alt f + : @id_tuple_with_alt_cps R A n value value_for_alt f = id_with_alt (value f) (value_for_alt f) + := eq_refl. Hint Rewrite @id_tuple_with_alt_cps_correct : uncps. -Lemma id_tuple_with_alt_proof_cps_correct {R A n} value value_for_alt pf f - : @id_tuple_with_alt_proof_cps R A n value value_for_alt pf f - = f (@id_tuple_with_alt_proof A n value value_for_alt pf). -Proof. destruct n; [ reflexivity | apply id_tuple'_with_alt_proof_cps_correct ]. Qed. -Hint Rewrite @id_tuple_with_alt_proof_cps_correct : uncps. + +Definition id_tuple'_with_alt_cps_correct_gen {R A n} + (value value_for_alt : forall R, (_ -> R) -> R) f + (Hvalue : value _ f = f (value _ id)) + : @id_tuple'_with_alt_cps R A n (value _) (value_for_alt _) f = f (id_tuple'_with_alt (value _ id) (value_for_alt _ id)). +Proof. + autorewrite with uncps. + rewrite ?unfold_id_tuple'_with_alt, ?unfold_id_tuple_with_alt, ?unfold_id_with_alt, Hvalue. + reflexivity. +Qed. +Hint Rewrite @id_tuple'_with_alt_cps_correct_gen : uncps. + +Definition id_tuple_with_alt_cps_correct_gen {R A n} + (value value_for_alt : forall R, (_ -> R) -> R) f + (Hvalue : value _ f = f (value _ id)) + : @id_tuple_with_alt_cps R A n (value _) (value_for_alt _) f = f (id_tuple_with_alt (value _ id) (value_for_alt _ id)). +Proof. + autorewrite with uncps. + rewrite ?unfold_id_tuple_with_alt, ?unfold_id_tuple_with_alt, ?unfold_id_with_alt, Hvalue. + reflexivity. +Qed. +Hint Rewrite @id_tuple_with_alt_cps_correct_gen : uncps. Lemma update_nth_id {T} i (xs:list T) : ListUtil.update_nth i id xs = xs. Proof. -- cgit v1.2.3