diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 20:45:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 20:45:24 -0400 |
| commit | 69fc6dabced75fd38eaf89c4186d7de0ccff93b8 (patch) | |
| tree | 51cbb232354ef058ea85b966e31dd368902950fa | |
| parent | 5e8fb524b8f3819a938eb00a6d7c2794e2dbdf56 (diff) | |
Add base_type_leb_total
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 26803e851..9f18f47e9 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -270,3 +270,10 @@ Lemma cast_back_flat_const_prod {var A B f} {V : _ * _} = (@cast_back_flat_const var A f (fst V) (fst v), @cast_back_flat_const var B f (snd V) (snd v)). Proof. reflexivity. Qed. + +Lemma base_type_leb_total + : forall x y : base_type, base_type_leb x y = true \/ base_type_leb y x = true. +Proof. + induction x, y; simpl; auto. + rewrite !Nat.leb_le; omega. +Qed. |