From 040cffe6c076ff3c20d9bbb7a577fbd4be8e3e16 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 12 Oct 2016 13:42:29 -0400 Subject: Generalize and simplify cast_word_refl --- src/Util/WordUtil.v | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'src/Util/WordUtil.v') diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 038a23ae6..a7eec6fb4 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -94,16 +94,8 @@ Definition setbit n {b} {H:n < b} (w:word b) : word b := Definition clearbit n {b} {H:n < b} (w:word b) : word b := wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w. -Lemma cast_word_refl {n} (w:word n) : @cast_word n n eq_refl w = w. -Proof. - induction w; - repeat match goal with - | _ => solve [trivial] - | _ => progress (simpl @cast_word;f_equal) - | |- context [@cast_word ?n ?n ?pf _ ] => - pattern pf; rewrite (Eqdep_dec.UIP_refl_nat n pf) - end. -Qed. +Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w. +Proof. induction w; simpl; auto using f_equal. Qed. Lemma wordToNnat_cast_word {n} (w:word n) m pf : wordToN (@cast_word n m pf w) = wordToN w. @@ -111,4 +103,4 @@ Proof. destruct pf; rewrite cast_word_refl; trivial. Qed. Lemma wordToN_cast_word {n} (w:word n) m pf : wordToN (@cast_word n m pf w) = wordToN w. -Proof. destruct pf; rewrite cast_word_refl; trivial. Qed. \ No newline at end of file +Proof. destruct pf; rewrite cast_word_refl; trivial. Qed. -- cgit v1.2.3