Commit 034bdcad authored by Johannes Kloos's avatar Johannes Kloos

Renamed subset_difference_in and moved to collection

parent 01f94618
...@@ -620,6 +620,9 @@ Section collection. ...@@ -620,6 +620,9 @@ Section collection.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma difference_disjoint X Y : X ## Y X Y X. Lemma difference_disjoint X Y : X ## Y X Y X.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma subset_difference_elem_of {x: A} {s: C} (inx: x s): s {[ x ]} s.
Proof. set_solver. Qed.
Lemma difference_mono X1 X2 Y1 Y2 : Lemma difference_mono X1 X2 Y1 Y2 :
X1 X2 Y2 Y1 X1 Y1 X2 Y2. X1 X2 Y2 Y1 X1 Y1 X2 Y2.
......
...@@ -27,13 +27,10 @@ Qed. ...@@ -27,13 +27,10 @@ Qed.
Section Fresh. Section Fresh.
Context `{FinCollection A C} `{Infinite A, !RelDecision (@elem_of A C _)}. Context `{FinCollection A C} `{Infinite A, !RelDecision (@elem_of A C _)}.
Lemma subset_difference_in {x: A} {s: C} (inx: x s): s {[ x ]} s.
Proof. set_solver. Qed.
Definition fresh_generic_body (s: C) (rec: s', s' s nat A) (n: nat) := Definition fresh_generic_body (s: C) (rec: s', s' s nat A) (n: nat) :=
let cand := inject n in let cand := inject n in
match decide (cand s) with match decide (cand s) with
| left H => rec _ (subset_difference_in H) (S n) | left H => rec _ (subset_difference_elem_of H) (S n)
| right _ => cand | right _ => cand
end. end.
Lemma fresh_generic_body_proper s (f g: y, y s nat A): Lemma fresh_generic_body_proper s (f g: y, y s nat A):
...@@ -64,7 +61,7 @@ Section Fresh. ...@@ -64,7 +61,7 @@ Section Fresh.
induction s as [s IH] using (well_founded_ind collection_wf); intro. induction s as [s IH] using (well_founded_ind collection_wf); intro.
setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body. setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
destruct decide as [case|case]; eauto with omega. destruct decide as [case|case]; eauto with omega.
destruct (IH _ (subset_difference_in case) (S n)) as [m [mbound [eqfix [notin inbelow]]]]. destruct (IH _ (subset_difference_elem_of case) (S n)) as [m [mbound [eqfix [notin inbelow]]]].
exists m; repeat split; auto with omega. exists m; repeat split; auto with omega.
- rewrite not_elem_of_difference, elem_of_singleton in notin. - rewrite not_elem_of_difference, elem_of_singleton in notin.
destruct notin as [?|?%inject_injective]; auto with omega. destruct notin as [?|?%inject_injective]; auto with omega.
......
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