From 08198ce4c75364b3e49e336fbb1e6bc6c0e9e054 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 Nov 2015 12:47:58 +0100
Subject: [PATCH] further improved unit for decidable agreement
---
lib/ModuRes/RAConstr.v | 35 ++++++++++++++---------------------
1 file changed, 14 insertions(+), 21 deletions(-)
diff --git a/lib/ModuRes/RAConstr.v b/lib/ModuRes/RAConstr.v
index 5edd522ab..244730df8 100644
--- a/lib/ModuRes/RAConstr.v
+++ b/lib/ModuRes/RAConstr.v
@@ -311,21 +311,17 @@ Section DecAgreement.
Inductive ra_dagree : Type :=
| dag_bottom
- | dag_unit
| dag_inj (t : T).
- Global Instance ra_unit_dagree : RA_unit _ :=
- fun x => if x isn't dag_unit then x else dag_unit.
+ Global Instance ra_unit_dagree : RA_unit ra_dagree :=
+ fun x => x.
Global Instance ra_valid_dag : RA_valid _ :=
fun x => match x with dag_bottom => False | _ => True end.
Global Instance ra_op_dag : RA_op _ :=
fun x y => match x, y with
| dag_inj t1, dag_inj t2 =>
- if eq_dec t1 t2 is left _ then dag_inj t1 else dag_bottom
- | dag_bottom , y => dag_bottom
- | x , dag_bottom => dag_bottom
- | dag_unit, y => y
- | x, dag_unit => x
+ if dec_eq t1 t2 is left _ then dag_inj t1 else dag_bottom
+ | _ , _ => dag_bottom
end.
Definition ra_eq_dag (x y: ra_dagree): Prop :=
@@ -347,36 +343,33 @@ Section DecAgreement.
- repeat (match goal with [ x : ra_dagree |- _ ] => destruct x end);
simpl in *; try discriminate || reflexivity || assumption; [].
unfold ra_op, ra_op_dag.
- destruct (eq_dec t2 t0), (eq_dec t1 t); simpl; auto; exfalso; apply n; congruence.
+ destruct (dec_eq t2 t0), (dec_eq t1 t); simpl; auto; exfalso; apply n; congruence.
- repeat (match goal with [ x : ra_dagree |- _ ] => destruct x end);
simpl in *; try discriminate || reflexivity || assumption;
compute; try destruct (eq_dec _ _); try reflexivity; [].
destruct (eq_dec t0 t), (eq_dec t1 t0), (eq_dec t1 t); simpl; auto; exfalso; apply n; congruence.
- destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0);
try reflexivity; auto; try contradiction; symmetry in e; contradiction.
- - destruct t; try reflexivity; []. rewrite/ra_unit/ra_op/=. by case: (eq_dec t t).
+ - destruct t; try reflexivity; []. rewrite/ra_unit/ra_op/=. by rewrite DecEq_refl.
- destruct x, y; simpl; firstorder; now inversion H.
- - case Ht: t => [|| t1]; [by exists dag_unit | by exists (1 t'); case: t' |].
- case Ht': t' => [|| t2]; rewrite/ra_unit/ra_op/=.
+ - case Ht: t => [| t1]; [by exists (1 t'); case: t' |].
+ case Ht': t' => [| t2]; rewrite/ra_unit/ra_op/=.
+ by exists dag_bottom.
- + by exists (dag_inj t1); case: (eq_dec t1 t1).
- + case: (eq_dec t1 t2); [by exists dag_unit|by exists dag_bottom].
+ + case: (dec_eq t1 t2); [|by exists dag_bottom]. exists (dag_inj t1).
+ by rewrite DecEq_refl.
- destruct t; reflexivity.
- destruct x, y; simpl; firstorder; now inversion H.
- destruct t1, t2; try contradiction; now constructor.
Qed.
- Lemma ra_sep_dag_gen {t r} : ↓dag_inj t · r -> r = dag_unit \/ r = dag_inj t.
+ Lemma ra_sep_dag_gen {t r} : ↓dag_inj t · r -> r = dag_inj t.
Proof.
- case: r; [done | by left|] => t' Hv; right; f_equal; move: Hv.
- by rewrite/ra_op/=; case: (eq_dec t t').
+ case: r; [done |] => t' Hv; f_equal; move: Hv.
+ by rewrite/ra_op/=; case: (dec_eq t t').
Qed.
Lemma ra_sep_dag {t t'} : ↓dag_inj t · dag_inj t' -> t = t'.
- Proof. by move/ra_sep_dag_gen => [? | [->]]. Qed.
-
- Global Instance ra_vira_dag : VIRA ra_dagree.
- Proof. by exists dag_unit. Qed.
+ Proof. by move/ra_sep_dag_gen => [ ->]. Qed.
End DecAgreement.
--
GitLab