From 5efc05b747b6edcdbd2c298855d9de53d8567369 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 13 Jun 2018 15:18:28 -0400 Subject: Add PrimitiveHList, PrimitiveProd --- src/Util/PrimitiveHList.v | 18 +++++ src/Util/PrimitiveProd.v | 201 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 219 insertions(+) create mode 100644 src/Util/PrimitiveHList.v create mode 100644 src/Util/PrimitiveProd.v (limited to 'src/Util') diff --git a/src/Util/PrimitiveHList.v b/src/Util/PrimitiveHList.v new file mode 100644 index 000000000..356861ebe --- /dev/null +++ b/src/Util/PrimitiveHList.v @@ -0,0 +1,18 @@ +Require Import Coq.Lists.List. +Require Import Crypto.Util.PrimitiveProd. + +Fixpoint hlist {A} (P : A -> Type) (ls : list A) : Type + := match ls return Type with + | nil => unit + | cons x xs => P x * @hlist A P xs + end%type. +Fixpoint split_list {A P} (ls : list (@sigT A P)) : { ls : list A & hlist P ls } + := match ls with + | nil => existT _ nil tt + | cons x xs => let 'existT ls' hls' := @split_list A P xs in existT _ (cons (projT1 x) ls') (projT2 x, hls') + end. +Fixpoint combine_hlist {A P} (ls : list A) : hlist P ls -> list (@sigT A P) + := match ls return hlist P ls -> _ with + | nil => fun _ => nil + | cons x xs => fun '(Px, Pxs) => existT P x Px :: @combine_hlist A P xs Pxs + end. diff --git a/src/Util/PrimitiveProd.v b/src/Util/PrimitiveProd.v new file mode 100644 index 000000000..0e2748501 --- /dev/null +++ b/src/Util/PrimitiveProd.v @@ -0,0 +1,201 @@ +(** * Definition and classification of the [×] Type, with primitive projections *) +(** In this file, we classify the basic structure of [×] types ([prod] + in Coq). In particular, we classify equalities of non-dependent + pairs (inhabitants of [×] types), so that when we have an equality + between two such pairs, or when we want such an equality, we have + a systematic way of reducing such equalities to equalities at + simpler types. *) +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.IffT. +Require Import Crypto.Util.Equality. +Require Import Crypto.Util.GlobalSettings. + +Local Set Primitive Projections. + +Delimit Scope primproj_type_scope with primproj_type. +Delimit Scope primproj_scope with primproj. + +Module Import Primitive. + Record prod A B := pair { fst : A ; snd : B }. + Global Arguments pair {_ _}. + Global Arguments fst {_ _}. + Global Arguments snd {_ _}. + + Module Import Notations. + Notation "x * y" := (@prod x y) : type_scope. + Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + End Notations. + + Local Set Implicit Arguments. + Definition prod_beq A B (eq_A : A -> A -> bool) (eq_B : B -> B -> bool) (X Y : A * B) : bool + := let '(a, b) := X in let '(a', b') := Y in (eq_A a a' && eq_B b b')%bool. + Global Arguments prod_beq / . + Lemma prod_dec_bl A B eq_A eq_B + (A_bl : forall x y : A, eq_A x y = true -> x = y) + (B_bl : forall x y : B, eq_B x y = true -> x = y) + (x y : A * B) + : prod_beq eq_A eq_B x y = true -> x = y. + Proof. + destruct x as [a b], y as [a' b']. + specialize (A_bl a a'); specialize (B_bl b b'). + cbn; intro H; destruct A_bl; [ | destruct B_bl; [ | reflexivity ] ]; + edestruct eq_A; edestruct eq_B; cbn in *; try reflexivity; try assumption. + Defined. + Lemma prod_dec_lb A B eq_A eq_B + (A_lb : forall x y : A, x = y -> eq_A x y = true) + (B_lb : forall x y : B, x = y -> eq_B x y = true) + (x y : A * B) + : x = y -> prod_beq eq_A eq_B x y = true. + Proof. + intro H; specialize (A_lb _ _ (f_equal fst H)); specialize (B_lb _ _ (f_equal snd H)). + cbn in *; cbv [fst snd] in *. + rewrite A_lb, B_lb; reflexivity. + Defined. + Definition prod_eq_dec A B eq_A eq_B + (A_bl : forall x y : A, eq_A x y = true -> x = y) + (B_bl : forall x y : B, eq_B x y = true -> x = y) + (A_lb : forall x y : A, x = y -> eq_A x y = true) + (B_lb : forall x y : B, x = y -> eq_B x y = true) + (x y : A * B) + : {x = y} + {x <> y}. + Proof. + refine (let H := let b := @prod_beq A B eq_A eq_B x y in if b as b0 return ({b0 = true} + {b0 = false}) then left eq_refl else right eq_refl in + match H with + | left e => left (@prod_dec_bl A B eq_A eq_B A_bl B_bl x y e) + | right H' => right (fun e => _ (@prod_dec_lb A B eq_A eq_B A_lb B_lb x y e)) + end). + congruence. + Defined. +End Primitive. +Notation "x * y" := (@prod x%primproj_type y%primproj_type) : primproj_type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x%primproj y%primproj) .. z%primproj) : primproj_scope. +Import Primitive.Notations. + +Local Arguments f_equal {_ _} _ {_ _} _. + +Definition fst_pair {A B} (a:A) (b:B) : fst (a,b) = a := eq_refl. +Definition snd_pair {A B} (a:A) (b:B) : snd (a,b) = b := eq_refl. +Create HintDb cancel_primpair discriminated. Hint Rewrite @fst_pair @snd_pair : cancel_primpair. + +(** ** Equality for [prod] *) +Section prod. + (** *** Projecting an equality of a pair to equality of the first components *) + Definition fst_path {A B} {u v : prod A B} (p : u = v) + : fst u = fst v + := f_equal fst p. + + (** *** Projecting an equality of a pair to equality of the second components *) + Definition snd_path {A B} {u v : prod A B} (p : u = v) + : snd u = snd v + := f_equal snd p. + + (** *** Equality of [prod] is itself a [prod] *) + Definition path_prod_uncurried {A B : Type} (u v : prod A B) + (pq : prod (fst u = fst v) (snd u = snd v)) + : u = v. + Proof. + destruct u as [u1 u2], v as [v1 v2]; simpl in *. + destruct pq as [p q]. + destruct p, q; simpl in *. + reflexivity. + Defined. + + (** *** Curried version of proving equality of sigma types *) + Definition path_prod {A B : Type} (u v : prod A B) + (p : fst u = fst v) (q : snd u = snd v) + : u = v + := path_prod_uncurried u v (pair p q). + + (** *** Equivalence of equality of [prod] with a [prod] of equality *) + (** We could actually use [IsIso] here, but for simplicity, we + don't. If we wanted to deal with proofs of equality of × types + in dependent positions, we'd need it. *) + Definition path_prod_uncurried_iff {A B} + (u v : @prod A B) + : u = v <-> (prod (fst u = fst v) (snd u = snd v)). + Proof. + split; [ intro; subst; split; reflexivity | apply path_prod_uncurried ]. + Defined. + + (** *** Eta-expansion of [@eq (prod _ _)] *) + Definition path_prod_eta {A B} {u v : @prod A B} (p : u = v) + : p = path_prod_uncurried u v (fst_path p, snd_path p). + Proof. destruct p; reflexivity. Defined. + + (** *** Induction principle for [@eq (prod _ _)] *) + Definition path_prod_rect {A B} {u v : @prod A B} (P : u = v -> Type) + (f : forall p q, P (path_prod_uncurried u v (p, q))) + : forall p, P p. + Proof. intro p; specialize (f (fst_path p) (snd_path p)); destruct p; exact f. Defined. + Definition path_prod_rec {A B u v} (P : u = v :> @prod A B -> Set) := path_prod_rect P. + Definition path_prod_ind {A B u v} (P : u = v :> @prod A B -> Prop) := path_prod_rec P. +End prod. + +Lemma prod_iff_and (A B : Prop) : (A /\ B) <-> (A * B). +Proof. repeat (intros [? ?] || intro || split); assumption. Defined. + +Global Instance iff_prod_Proper + : Proper (iff ==> iff ==> iff) (fun A B => prod A B). +Proof. repeat intro; tauto. Defined. +Global Instance iff_iffTp_prod_Proper + : Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. +Proof. + intros ?? [?] ?? [?]; constructor; tauto. +Defined. +Global Instance iffTp_iff_prod_Proper + : Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1. +Proof. + intros ?? [?] ?? [?]; constructor; tauto. +Defined. +Global Instance iffTp_iffTp_prod_Proper + : Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. +Proof. + intros ?? [?] ?? [?]; constructor; tauto. +Defined. +Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances. + +(** ** Useful Tactics *) +(** *** [inversion_prod] *) +Ltac simpl_proj_pair_in H := + repeat match type of H with + | context G[fst (pair ?x ?p)] + => let G' := context G[x] in change G' in H + | context G[snd (pair ?x ?p)] + => let G' := context G[p] in change G' in H + end. +Ltac induction_path_prod H := + let H0 := fresh H in + let H1 := fresh H in + induction H as [H0 H1] using path_prod_rect; + simpl_proj_pair_in H0; + simpl_proj_pair_in H1. +Ltac inversion_prod_step := + match goal with + | [ H : _ = pair _ _ |- _ ] + => induction_path_prod H + | [ H : pair _ _ = _ |- _ ] + => induction_path_prod H + end. +Ltac inversion_prod := repeat inversion_prod_step. + +(** *** [subst_prod] *) +(** The tactic [subst_prod] is like [subst], but it works on equations + of the form [_ = (x, y)] and [(x, y) = _] for [x] and [y] + identifiers. *) +Ltac do_subst_prod A B x y := + is_var x; is_var y; + let H := fresh in + let xy := fresh x in + remember (@pair A B x y) as xy eqn:H; + assert (fst xy = x) by (subst xy; reflexivity); + assert (snd xy = y) by (subst xy; reflexivity); + subst x y; + clear H; try subst xy. +Ltac subst_prod_step := + match goal with + | [ H : _ = @pair ?A ?B ?x ?y |- _ ] => do_subst_prod A B x y + | [ H : @pair ?A ?B ?x ?y = _ |- _ ] => do_subst_prod A B x y + end. +Ltac subst_prod := repeat subst_prod_step. -- cgit v1.2.3