diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-12 10:10:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-12 10:10:19 +0000 |
| commit | 644bd3cfc92fa0ddded80566b25b8a11957f6edf (patch) | |
| tree | b393e62ca40e3c8632f95270caec96ce2b7f3ee2 /lib/Lattice.v | |
| parent | 45fc4cc348d2b8c4cc151a5e3ce3483f21a6ef78 (diff) | |
| download | compcert-kvx-644bd3cfc92fa0ddded80566b25b8a11957f6edf.tar.gz compcert-kvx-644bd3cfc92fa0ddded80566b25b8a11957f6edf.zip | |
Maps: revised TREE interface; added mucho derived properties and operations in Tree_Properties.
Lattice: adapted accordingly.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2147 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Lattice.v')
| -rw-r--r-- | lib/Lattice.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v index fd05b346..c4b55e90 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -141,11 +141,15 @@ Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. destruct x; destruct y; simpl; intro; try congruence. red; intro; simpl. - generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). - destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. + rewrite PTree.beq_correct in H. generalize (H p). + destruct (t0!p); destruct (t1!p); intuition. + apply L.beq_correct; auto. + apply L.eq_refl. red; intro; simpl. - generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). - destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. + rewrite PTree.beq_correct in H. generalize (H p). + destruct (t0!p); destruct (t1!p); intuition. + apply L.beq_correct; auto. + apply L.eq_refl. Qed. Definition ge (x y: t) : Prop := |