Commit 05eb175e authored by Johannes Kloos's avatar Johannes Kloos
Browse files

Fix the size of wg_guard unfolding

parent e1ae086f
...@@ -71,7 +71,7 @@ Section Fresh. ...@@ -71,7 +71,7 @@ Section Fresh.
apply inbelow; omega. apply inbelow; omega.
Qed. Qed.
Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix s 0. Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix 20 s 0.
Instance fresh_generic_spec: FreshSpec A C. Instance fresh_generic_spec: FreshSpec A C.
Proof. Proof.
...@@ -79,16 +79,16 @@ Section Fresh. ...@@ -79,16 +79,16 @@ Section Fresh.
- apply _. - apply _.
- intros * eqXY. - intros * eqXY.
unfold fresh, fresh_generic. unfold fresh, fresh_generic.
destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size X)) X 0) destruct (fresh_generic_fixpoint_spec 20 X 0)
as [mX [_ [-> [notinX belowinX]]]]. as [mX [_ [-> [notinX belowinX]]]].
destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size Y)) Y 0) destruct (fresh_generic_fixpoint_spec 20 Y 0)
as [mY [_ [-> [notinY belowinY]]]]. as [mY [_ [-> [notinY belowinY]]]].
destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto. destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
+ contradict notinX; rewrite eqXY; apply belowinY; omega. + contradict notinX; rewrite eqXY; apply belowinY; omega.
+ contradict notinY; rewrite <- eqXY; apply belowinX; omega. + contradict notinY; rewrite <- eqXY; apply belowinX; omega.
- intro. - intro.
unfold fresh, fresh_generic. unfold fresh, fresh_generic.
destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size X)) X 0) destruct (fresh_generic_fixpoint_spec 20 X 0)
as [m [_ [-> [notinX belowinX]]]]; auto. as [m [_ [-> [notinX belowinX]]]]; auto.
Qed. Qed.
End Fresh. End Fresh.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment