diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-12 13:42:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-12 13:42:29 -0400 |
| commit | 040cffe6c076ff3c20d9bbb7a577fbd4be8e3e16 (patch) | |
| tree | 1b999a270f943b6332f752a27ab69240b3e15b65 /src/Util/WordUtil.v | |
| parent | e4343af559e114e55e33329ddaaf47560b93b1d9 (diff) | |
Generalize and simplify cast_word_refl
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 14 |
1 files changed, 3 insertions, 11 deletions
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. |