Merge branch 'master' of github.mit.edu:plv/fiat-crypto

2 files changed, 72 insertions, 13 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 6826f638e..abfc2499c 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -228,3 +228,26 @@ Ltac destruct_sig_matcher HT :=
   end.
 Ltac destruct_sig := destruct_all_matches destruct_sig_matcher.
 Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher.
+
+(** If [tac_in H] operates in [H] and leaves side-conditions before
+    the original goal, then
+    [side_conditions_before_to_side_conditions_after tac_in H] does
+    the same thing to [H], but leaves side-conditions after the
+    original goal. *)
+Ltac side_conditions_before_to_side_conditions_after tac_in H :=
+  let HT := type of H in
+  let HTT := type of HT in
+  let H' := fresh in
+  rename H into H';
+  let HT' := fresh in
+  evar (HT' : HTT);
+  cut HT';
+  [ subst HT'; intro H
+  | tac_in H';
+    [ ..
+    | subst HT'; eexact H' ] ];
+  instantiate; (* required in 8.4 for the [move] to succeed, because evar dependencies *)
+  [ (* We preserve the order of the hypotheses.  We need to do this
+       here, after evars are instantiated, and not above. *)
+    move H after H'; clear H'
+  | .. ].
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index d08c52c82..42a242fad 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -26,23 +26,39 @@ Definition to_list {T} (n:nat) : tuple T n -> list T :=
   | S n' => fun xs : tuple T (S n') => to_list' n' xs
   end.
 
-Fixpoint from_list' {T} (x:T) (xs:list T) : tuple' T (length xs) :=
-  match xs with
-  | nil => x
-  | (y :: xs')%list => (from_list' y xs', x)
+Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n :=
+  match n return _ with
+  | 0 =>
+    match xs return (length xs = 0 -> tuple' T 0) with
+    | nil => fun _ => y
+    | _ => _ (* impossible *)
+    end
+  | S n' =>
+    match xs return (length xs = S n' -> tuple' T (S n')) with
+    | cons x xs' => fun _ => (from_list' x n' xs' _, y)
+    | _ => _ (* impossible *)
+    end
   end.
 
-Definition from_list {T} (xs:list T) : tuple T (length xs) :=
-  match xs as l return (tuple T (length l)) with
-  | nil => tt
-  | (t :: xs')%list => from_list' t xs'
-  end.
+Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n :=
+match n return _ with
+| 0 =>
+    match xs return (length xs = 0 -> tuple T 0) with
+    | nil => fun _ : 0 = 0 => tt
+    | _ => _ (* impossible *)
+    end
+| S n' =>
+    match xs return (length xs = S n' -> tuple T (S n')) with
+    | cons x xs' => fun _ => from_list' x n' xs' _
+    | _ => _ (* impossible *)
+    end
+end.
 
-Lemma to_list_from_list : forall {T} (xs:list T), to_list (length xs) (from_list xs) = xs.
+Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
 Proof.
-  destruct xs; auto; simpl.
-  generalize dependent t.
-  induction xs; auto; simpl; intros; f_equal; auto.
+  destruct xs; simpl; intros; subst; auto.
+  generalize dependent t. simpl in *.
+  induction xs; simpl in *; intros; congruence.
 Qed.
 
 Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n.
@@ -52,6 +68,26 @@ Proof.
   destruct xs; simpl in *; eauto.
 Qed.
 
+Lemma from_list'_to_list' : forall T n (xs:tuple' T n),
+    forall x xs' pf, to_list' n xs = cons x xs' ->
+      from_list' x n xs' pf = xs.
+Proof.
+  induction n; intros.
+  { simpl in *. injection H; clear H; intros; subst. congruence. }
+  { destruct xs eqn:Hxs;
+    destruct xs' eqn:Hxs';
+    injection H; clear H; intros; subst; try discriminate.
+    simpl. f_equal. eapply IHn. assumption. }
+Qed.
+
+Lemma from_list_to_list : forall {T n} (xs:tuple T n) pf, from_list n (to_list n xs) pf = xs.
+Proof.
+  destruct n; auto; intros; simpl in *.
+  { destruct xs; auto. }
+  { destruct (to_list' n xs) eqn:H; try discriminate.
+    eapply from_list'_to_list'; assumption. }
+Qed.
+
 Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop.
   destruct n; simpl @tuple' in *.
   { exact (R a b). }