Library set_relation
This file can be split into two parts.
The first part implements a function computing inefficiently the
reflexive transitive closure of a relation set_rel_power.
This function is proved to correctly implement the inductive definition
of the reflexive transitive closure of relation (clos_refl_trans) under certain
hypotheses set_rel_clos_relation_iff.
The second part defines a more efficient version and proves it correct against
the first implementation (set_rel_clos_relation_iff).
Require Import Bool.
Require Import List. Import ListNotations.
Require Import Sorted.
Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Import Setoid.
Require Export sflib.
Require Export set.
Require Export set2.
Require Import last.
Section relation.
Context `{DS:DecidableType} (d:relation A) (r:A → A → bool).
Definition set_stable (x:set A) :=
∀ l', set_In l' x → ∀ l, d l l' → set_In l x.
Fixpoint set_rel_power (n:nat) (x:set A) (a1 a2 : A) :=
match n with
| 0 ⇒ if DS_decide a1 a2 then true else false
| S n' ⇒
negb (set_test_empty
(set_filter
(fun a ⇒ r a1 a && (set_rel_power n' x a a2)) x))
end.
Fixpoint set_rel_clos_refl_trans_aux (n:nat) (x:set A) (a1 a2 : A) :=
match n with
| 0 ⇒ set_rel_power 0 x a1 a2
| S n' ⇒ set_rel_power n x a1 a2 || set_rel_clos_refl_trans_aux n' x a1 a2
end.
Definition set_rel_clos_refl_trans (x:set A) :=
set_rel_clos_refl_trans_aux (set_size x) x.
Definition inverse (x:set A) (a:A) :=
set_filter (fun a' ⇒ r a' a) x.
Definition set_inverse (x y:set A) :=
set_filter (fun a' ⇒
negb (set_test_empty (set_filter (fun a ⇒ r a' a) y))) x.
Lemma inverse_r : ∀ x a a', set_In a' (inverse x a) ↔
set_In a' x ∧ r a' a = true.
Proof.
intros. unfold inverse. rewrite set_filter_In. reflexivity.
Qed.
Lemma set_inverse_r : ∀ x y a,
set_In a (set_inverse x y) ↔ set_In a x ∧
(∃ a', set_In a' y ∧ r a a' = true).
Proof.
intros.
unfold set_inverse. rewrite set_filter_In.
rewrite negb_true_iff. rewrite set_not_empty_In.
split; intros.
- destruct H. inversion H0 as [a0 H1].
apply set_filter_In in H1. destruct H1.
split. assumption. ∃ a0. split; assumption.
- destruct H. inversion H0 as [a0 H1].
destruct H1. split. assumption.
∃ a0. apply set_filter_In. split; assumption.
Qed.
Lemma set_inverse_singleton : ∀ x a,
set_same (set_inverse x (set_singleton a)) (inverse x a).
Proof.
intros. unfold set_same; unfold set_incl; split; intros.
- apply set_inverse_r in H. apply inverse_r.
destruct H. inversion H0 as [a' H1].
destruct H1. apply set_singleton_In in H1. subst. split; assumption.
- apply inverse_r in H. apply set_inverse_r.
destruct H. split. assumption.
∃ a. split. apply set_singleton_In. reflexivity. assumption.
Qed.
Lemma set_rel_power_clos : ∀ n x a1 a2,
set_rel_power n x a1 a2 = true →
set_rel_clos_refl_trans_aux n x a1 a2 = true.
Proof.
intros. destruct n.
apply H.
simpl in ×. apply orb_true_intro.
left; assumption.
Qed.
Lemma set_rel_clos_relation_aux :
(∀ a1 a2, r a1 a2 = true → d a1 a2) →
∀ x,
∀ a1 a2 n, set_rel_clos_refl_trans_aux n x a1 a2 = true →
clos_refl_trans A d a1 a2.
Proof.
intros. revert a1 a2 H0.
induction n; intros.
- simpl in H0. destruct (DS_decide a1 a2).
subst. apply rt_refl.
inversion H0.
- simpl in H0. apply orb_true_iff in H0. destruct H0.
apply negb_true_iff in H0.
apply set_not_empty_In in H0. inversion H0 as [a H2].
apply set_filter_In in H2. rewrite andb_true_iff in H2.
destruct H2 as [H2 [H3 H4]].
apply rt_trans with (y:=a). apply rt_step. apply H; assumption.
apply IHn. apply set_rel_power_clos. assumption.
apply IHn; assumption.
Qed.
Lemma set_rel_clos_relation :
(∀ a1 a2, r a1 a2 = true → d a1 a2) →
∀ x,
∀ a1 a2, set_rel_clos_refl_trans x a1 a2 = true →
clos_refl_trans A d a1 a2.
Proof.
intros.
apply set_rel_clos_relation_aux with (x:=x) (n:=set_size x); assumption.
Qed.
Lemma set_rel_power_clos_le : ∀ m n x a1 a2,
m ≤ n →
set_rel_power m x a1 a2 = true →
set_rel_clos_refl_trans_aux n x a1 a2 = true.
Proof. intros m n. revert m.
induction n; intros.
- apply set_rel_power_clos. inversion H. subst. assumption.
- inversion H.
+ apply set_rel_power_clos. subst; assumption.
+ simpl. apply orb_true_iff. right. apply IHn with (m:=m); assumption.
Qed.
Fixpoint appears_in (a:A) (l:list A) :=
match l with
| [] ⇒ false
| a'::l' ⇒ if DS_decide a a' then true else appears_in a l'
end.
Fixpoint find_last (a:A) (l:list A) :=
match l with
| [] ⇒ []
| a'::l' ⇒ if appears_in a l' then find_last a l'
else if DS_decide a a' then (a'::l') else []
end.
Lemma find_last_decrease : ∀ a l,
length (find_last a l) ≤ length l.
Proof.
intros. induction l.
apply le_n.
simpl. destruct (appears_in a l).
apply le_S. assumption.
destruct (DS_decide a a0).
apply le_n.
apply le_0_n.
Qed.
Function remove_cycles (l:list A) {measure length} :=
match l with
| [] ⇒ []
| a'::l' ⇒ if appears_in a' l' then remove_cycles (find_last a' l')
else a'::remove_cycles l'
end.
Proof.
intros. simpl. apply le_n_S. apply find_last_decrease.
intros. simpl. apply le_n.
Qed.
Inductive repeat : list A → Prop :=
| repeat_here : ∀ a l, appears_in a l = true → repeat (a::l)
| repeat_after : ∀ a l, repeat l → repeat (a::l).
Inductive include : list A → list A → Prop :=
| include_nil : include [] []
| include_here : ∀ a l l', include l l' → include (a::l) (a::l')
| include_after : ∀ a l l', include l l' → include l (a::l').
Lemma include_refl : ∀ l, include l l.
Proof. induction l. constructor. apply include_here; assumption.
Qed.
Lemma include_trans : ∀ l1 l2 l3, include l1 l2 → include l2 l3 →
include l1 l3.
Proof.
intros l1 l2 l3. revert l1 l2.
induction l3; intros.
inversion H0. subst. inversion H. constructor.
inversion H0; subst.
inversion H; subst.
apply include_here. apply IHl3 with (l2:=l); assumption.
apply include_after. apply IHl3 with (l2:=l); assumption.
apply include_after. apply IHl3 with (l2:=l2); assumption.
Qed.
Lemma include_nil_l : ∀ l, include [] l.
Proof. intros.
induction l. constructor. apply include_after; assumption.
Qed.
Lemma include_appears_in : ∀ l1 l2,
include l1 l2 → ∀ a, appears_in a l1 = true → appears_in a l2 = true.
Proof.
intros. induction H.
- inversion H0.
- simpl. simpl in H0. destruct (DS_decide a a0).
reflexivity. apply IHinclude; assumption.
- simpl. destruct (DS_decide a a0). reflexivity.
apply IHinclude; assumption.
Qed.
Lemma include_incl : ∀ l1 l2,
include l1 l2 → incl l1 l2.
Proof.
intros. induction H.
- unfold incl; intros. inversion H.
- unfold incl; intros. destruct H0.
+ subst a0. left; reflexivity.
+ right; apply IHinclude; assumption.
- apply incl_tl. assumption.
Qed.
Lemma find_last_include : ∀ l a,
include (find_last a l) l.
Proof.
intros. induction l.
- apply include_nil.
- simpl. destruct (appears_in a l).
+ apply include_after. assumption.
+ destruct (DS_decide a a0).
× apply include_refl.
× apply include_nil_l.
Qed.
Lemma remove_cycles_include : ∀ l,
include (remove_cycles l) l.
Proof. intros.
functional induction (remove_cycles l).
- apply include_nil.
- apply include_trans with (l2:=find_last a' l').
assumption. apply include_after. apply find_last_include.
- apply include_here. assumption.
Qed.
Lemma repeat_include : ∀ l1 l2,
include l1 l2 → repeat l1 → repeat l2.
Proof.
intros.
induction H.
- assumption.
- inversion H0.
+ apply repeat_here.
apply include_appears_in with (l1:=l); assumption.
+ apply repeat_after. apply IHinclude. assumption.
- apply repeat_after. apply IHinclude; assumption.
Qed.
Lemma remove_cycles_no_repeat : ∀ l,
¬ repeat (remove_cycles l).
Proof.
intros. functional induction (remove_cycles l); intros contra.
- inversion contra.
- contradiction.
- apply IHl0. inversion contra. apply include_appears_in with (l2:=l') in H0.
rewrite e0 in H0. inversion H0. apply remove_cycles_include.
assumption.
Qed.
Lemma no_repeat_bound_aux : ∀ x a l,
¬ repeat (a::l) → Forall (fun a' ⇒ set_In a' x) (a::l) →
Forall (fun a' ⇒ set_In a' (set_remove a x)) l.
Proof.
intros x a l. revert x a.
induction l; intros.
- constructor.
- constructor.
+ apply set_remove_not_In.
split. inversion H0. inversion H4. assumption.
intros contra. apply H. subst. apply repeat_here. simpl.
destruct (DS_decide a0 a0). reflexivity. exfalso. apply n; reflexivity.
+ apply IHl.
× intros contra. apply H. inversion contra.
subst. apply repeat_here. simpl. destruct (DS_decide a0 a).
reflexivity. assumption.
apply repeat_after. apply repeat_after. assumption.
× inversion H0. inversion H4. constructor; assumption.
Qed.
Lemma no_repeat_bound : ∀ x l,
Forall (fun a ⇒ set_In a x) l →
¬ repeat l → length l ≤ set_size x.
Proof.
intros x l. revert x.
induction l; intros.
apply le_0_n.
pose proof H.
apply no_repeat_bound_aux in H1.
apply IHl in H1. rewrite set_size_In_remove in H1.
simpl. apply le_n_S in H1.
destruct (set_size x) eqn:Heqsize. apply set_size_0_empty in Heqsize.
rewrite set_empty_not_In in Heqsize. pose proof (Heqsize a).
inversion H; contradiction.
simpl in H1. rewrite <- minus_n_O in H1. assumption.
inversion H; assumption. intros contra. apply H0. apply repeat_after.
assumption. assumption.
Qed.
Lemma set_rel_power_list : ∀ n x a1 a2, set_In a1 x → set_In a2 x →
set_rel_power n x a1 a2 = true →
∃ l, length l = S n ∧ hd a1 l = a1 ∧ last l a2 = a2 ∧
Forall (fun a ⇒ set_In a x) l ∧
Sorted (fun a a' ⇒ Is_true (r a a')) l.
Proof.
intros n. induction n; intros.
- simpl in H1. destruct (DS_decide a1 a2).
∃ [a1]. repeat split. rewrite e. reflexivity.
constructor. assumption. constructor.
constructor; constructor.
inversion H1.
- simpl in H1. apply negb_true_iff in H1.
apply set_not_empty_In in H1. inversion H1 as [a H2].
apply set_filter_In in H2. rewrite andb_true_iff in H2.
destruct H2 as [H2 [H3 H4]].
apply IHn in H4. inversion H4 as [l H5].
destruct H5 as [H5 [H6 [H7 [H8 H9]]]].
∃ (a1::l). repeat split.
+ simpl. rewrite H5. reflexivity.
+ rewrite last_cons_not_nil. assumption. destruct l. inversion H5. discriminate.
+ constructor; assumption.
+ constructor. assumption.
destruct l. inversion H5. inversion H9. constructor. simpl in H6.
subst a0. rewrite H3. simpl. trivial.
+ assumption.
+ assumption.
Qed.
Lemma set_list_rel_power : ∀ n x a1 a2 l,
length l = S n → hd a1 l = a1 → last l a2 = a2 →
Forall (fun a ⇒ set_In a x) l →
Sorted (fun a a' ⇒ Is_true (r a a')) l → set_rel_power n x a1 a2 = true.
Proof.
intros n. induction n; intros.
- simpl. destruct (DS_decide a1 a2). reflexivity.
destruct l. inversion H. destruct l. simpl in H0, H1. subst. contradiction.
inversion H.
- simpl. apply negb_true_iff. apply set_not_empty_In.
destruct l. inversion H. destruct l. inversion H.
∃ a0. apply set_filter_In. rewrite andb_true_iff.
repeat split. inversion H2. inversion H7. assumption.
inversion H3. inversion H7. simpl in H0. subst a. destruct (r a1 a0).
reflexivity. inversion H9.
apply IHn with (l:=a0::l). simpl in H. apply eq_add_S in H.
simpl; assumption.
reflexivity.
rewrite last_cons_not_nil in H1. assumption. discriminate.
inversion H2; assumption.
inversion H3; assumption.
Qed.
Lemma include_forall : ∀ l l' P,
include l l' → Forall P l' → Forall P l.
Proof.
intros. induction H.
- constructor.
- inversion H0. constructor. assumption. apply IHinclude. assumption.
- apply IHinclude. inversion H0; assumption.
Qed.
Lemma set_list_too_long : ∀ (x:set A) (l : list A),
Forall (fun a ⇒ set_In a x) l →
length (remove_cycles l) ≤ set_size x.
Proof.
intros.
apply no_repeat_bound.
apply include_forall with (l':=l). apply remove_cycles_include.
assumption.
apply remove_cycles_no_repeat.
Qed.
Lemma find_last_stays_sorted : ∀ a l P,
Sorted P l → Sorted P (find_last a l).
Proof.
intros. induction l.
- simpl. constructor.
- simpl. inversion H. destruct (appears_in a l) eqn:Heqin.
apply IHl; assumption. destruct (DS_decide a a0).
assumption. constructor.
Qed.
Lemma find_last_keeps_head : ∀ a l a',
l ≠ [] → appears_in a l = true → hd a' (find_last a l) = a ∧
find_last a l ≠ [].
Proof.
intros. induction l.
inversion H0.
assert (l = [] ∨ l ≠ []). destruct l. left; reflexivity.
right; discriminate.
destruct H1.
simpl in H0. subst. simpl. destruct (DS_decide a a0).
subst. simpl. split. reflexivity. discriminate. inversion H0.
simpl. destruct (appears_in a l) eqn:Heqin.
apply IHl. assumption. reflexivity.
destruct (DS_decide a a0). subst; split. reflexivity. discriminate.
simpl in H0. destruct (DS_decide a a0). contradiction. rewrite H0 in Heqin.
inversion Heqin.
Qed.
Lemma remove_cycles_keeps_head : ∀ a l,
l ≠ [] → hd a (remove_cycles l) = hd a l.
Proof.
intros. functional induction (remove_cycles l).
- reflexivity.
- assert (l' = [] ∨ l' ≠ []). destruct l'. left; reflexivity.
right; discriminate.
destruct H0. subst. inversion e0.
rewrite IHl0. simpl. apply find_last_keeps_head; assumption.
apply find_last_keeps_head; assumption.
- reflexivity.
Qed.
Lemma find_last_keeps_last : ∀ a l a',
l ≠ [] → appears_in a l = true → last (find_last a l) a' = last l a' ∧
find_last a l ≠ [].
Proof.
intros. induction l.
- inversion H0.
- assert (l = [] ∨ l ≠ []). destruct l. left; reflexivity.
right; discriminate.
destruct H1.
+ subst. simpl in H0. simpl. destruct (DS_decide a a0).
split. reflexivity. discriminate. inversion H0.
+ rewrite last_cons_not_nil. simpl. simpl in H0.
destruct (appears_in a l) eqn:Heqin. apply IHl. assumption. reflexivity.
destruct (DS_decide a a0). subst. split. apply last_cons_not_nil; assumption.
discriminate.
inversion H0. assumption.
Qed.
Lemma remove_cycles_keeps_last : ∀ a l,
l ≠ [] → last (remove_cycles l) a = last l a ∧ remove_cycles l ≠ [].
Proof.
intros. functional induction (remove_cycles l).
- split. reflexivity. assumption.
- assert (l' = [] ∨ l' ≠ []). destruct l'. left; reflexivity.
right; discriminate.
destruct H0.
+ subst. inversion e0.
+ pose proof H0. apply (find_last_keeps_last a' _ a') in H0.
destruct H0. apply IHl0 in H2. destruct H2. rewrite H2.
rewrite last_cons_not_nil by assumption. split.
apply find_last_keeps_last; assumption. assumption. assumption.
- destruct l' eqn:Heql'.
+ rewrite remove_cycles_equation. split. reflexivity. discriminate.
+ split. rewrite last_cons_not_nil. rewrite last_cons_not_nil. apply IHl0.
discriminate. discriminate. apply IHl0. discriminate.
discriminate.
Qed.
Lemma remove_cycles_stays_sorted : ∀ l P,
Sorted P l → Sorted P (remove_cycles l).
Proof.
intros. functional induction (remove_cycles l).
- constructor.
- apply IHl0. apply find_last_stays_sorted. inversion H; assumption.
- inversion H. constructor. apply IHl0. assumption.
subst. destruct l'.
rewrite remove_cycles_equation. constructor.
pose proof (remove_cycles_keeps_head a' (a::l')).
destruct (remove_cycles (a::l')). constructor.
constructor. simpl in H0. rewrite H0. inversion H3. assumption.
discriminate.
Qed.
Lemma find_last_nil : ∀ a l,
find_last a l = [] ↔ l = [] ∨ appears_in a l = false.
Proof.
split; intros.
- induction l.
+ left; reflexivity.
+ right. simpl. simpl in H.
destruct (appears_in a l) eqn:Heqin.
× destruct l. inversion Heqin. apply IHl in H. destruct H; inversion H.
× destruct (DS_decide a a0). inversion H. reflexivity.
- destruct H.
+ subst. reflexivity.
+ induction l. reflexivity. simpl.
simpl in H. destruct (DS_decide a a0). inversion H.
rewrite H. reflexivity.
Qed.
Lemma remove_cycles_nil : ∀ l,
remove_cycles l = [] ↔ l = [].
Proof.
split; intros.
- functional induction (remove_cycles l).
+ reflexivity.
+ apply IHl0 in H. apply find_last_nil in H. destruct H.
subst. inversion e0. rewrite H in e0. inversion e0.
+ inversion H.
- subst; rewrite remove_cycles_equation; reflexivity.
Qed.
Lemma set_rel_power_size_aux : ∀ (x:set A) (a1 a2 : A) n,
set_In a1 x → set_In a2 x →
set_rel_power n x a1 a2 = true →
∃ m, m < set_size x ∧ set_rel_power m x a1 a2 = true.
Proof.
intros.
apply set_rel_power_list in H1; try assumption.
inversion H1 as [l H2].
repeat destruct H2 as [?H H2].
assert (l ≠ []). { destruct l. inversion H3. discriminate. }
remember (length (remove_cycles l)) as m.
destruct m. symmetry in Heqm. apply length_zero_iff_nil in Heqm.
destruct l. inversion H3. rewrite remove_cycles_nil in Heqm.
inversion Heqm.
∃ m. split. unfold lt.
rewrite Heqm. apply set_list_too_long. assumption.
apply set_list_rel_power with (l:=remove_cycles l).
rewrite Heqm; reflexivity.
rewrite remove_cycles_keeps_head; assumption.
rewrite <- H5 at 2.
apply remove_cycles_keeps_last; assumption.
apply include_forall with (l':=l). apply remove_cycles_include.
assumption.
apply remove_cycles_stays_sorted. assumption.
Qed.
Lemma set_rel_power_add : ∀ (x:set A) (a1 a2 a3:A) n m,
set_rel_power n x a1 a2 = true →
set_rel_power m x a2 a3 = true →
set_rel_power (n+m) x a1 a3 = true.
Proof.
intros x a1 a2 a3 n. revert x a1 a2 a3. induction n; intros.
- simpl in H. destruct (DS_decide a1 a2). subst. simpl.
assumption. inversion H.
- simpl in H. simpl.
apply negb_true_iff. apply set_not_empty_In.
apply negb_true_iff in H. apply set_not_empty_In in H.
inversion H as [a H1]. ∃ a.
apply set_filter_In. rewrite andb_true_iff.
apply set_filter_In in H1. rewrite andb_true_iff in H1.
destruct H1 as [H1 [H2 H3]].
apply (IHn x a a2 a3 m) in H3; try assumption.
repeat split; assumption.
Qed.
Lemma set_rel_add_power : ∀ x a1 a3 n m,
set_rel_power (n+m) x a1 a3 = true →
∃ a2, set_rel_power n x a1 a2 = true ∧
set_rel_power m x a2 a3 = true.
Proof.
intros x a1 a3 n. revert x a1 a3. induction n; intros.
- ∃ a1. split.
+ simpl. destruct (DS_decide a1 a1).
reflexivity. contradiction n; reflexivity.
+ simpl in H. assumption.
- simpl in H. rewrite negb_true_iff in H. apply set_not_empty_In in H.
destruct H as [a2 H]. rewrite set_filter_In in H.
rewrite andb_true_iff in H. destruct H as [H [H0 H1]].
apply IHn in H1. destruct H1 as [a4 [H1 H2]].
∃ a4. split.
+ simpl. rewrite negb_true_iff. apply set_not_empty_In.
∃ a2. rewrite set_filter_In. rewrite andb_true_iff.
repeat split; assumption.
+ assumption.
Qed.
Lemma set_rel_power_size : ∀ (x:set A) (a1 a2 : A) n,
set_rel_power n x a1 a2 = true →
∃ m, m ≤ set_size x ∧ set_rel_power m x a1 a2 = true.
Proof.
intros. destruct n.
- ∃ 0. split. apply le_0_n. assumption.
- destruct n.
+ ∃ 1. split. destruct (set_size x) eqn:Heqsize.
simpl in H. rewrite negb_true_iff in H. rewrite set_not_empty_In in H.
destruct H as [a H]. rewrite set_filter_In in H. destruct H as [H _].
apply set_size_0_empty in Heqsize. apply set_test_empty_correct in Heqsize.
apply Heqsize in H. inversion H.
apply le_n_S. apply le_0_n. assumption.
+ replace (S (S n)) with (1 + (n + 1)) in H
by (rewrite PeanoNat.Nat.add_assoc;
rewrite PeanoNat.Nat.add_comm; reflexivity).
apply set_rel_add_power in H. destruct H as [a1' [H H0]].
pose proof H as Hpower.
pose proof H0.
apply set_rel_add_power in H1. destruct H1 as [a2' [H1 H2]].
simpl in H. rewrite negb_true_iff in H. rewrite set_not_empty_In in H.
destruct H as [a0 H]. rewrite set_filter_In in H.
rewrite andb_true_iff in H. decompose [and] H; clear H.
destruct (DS_decide a0 a1'); [|discriminate H6]. subst a0.
simpl in H2. rewrite negb_true_iff in H2. rewrite set_not_empty_In in H2.
destruct H2 as [a0 H2]. rewrite set_filter_In in H2.
rewrite andb_true_iff in H2. decompose [and] H2; clear H2.
destruct (DS_decide a0 a2); [|discriminate H8]. subst a0.
apply set_rel_power_size_aux in H0; try assumption.
destruct H0 as [m [H9 H10]].
∃ (S m). split. assumption.
replace (S m) with (1 + m) by reflexivity.
apply set_rel_power_add with (a2:=a1'); assumption.
Qed.
Lemma set_rel_clos_power_aux : ∀ x a1 a2 n,
set_rel_clos_refl_trans_aux n x a1 a2 = true →
∃ m, m ≤ n ∧ set_rel_power m x a1 a2 = true.
Proof.
intros. induction n.
- simpl in H.
∃ 0. simpl. destruct (DS_decide a1 a2). subst. split. apply le_n.
reflexivity. inversion H.
- simpl in H. apply orb_true_iff in H. destruct H.
+ ∃ (S n). split. apply le_n. simpl.
apply negb_true_iff in H. apply negb_true_iff.
apply set_not_empty_In in H. apply set_not_empty_In.
inversion H as [a H0]. ∃ a. assumption.
+ apply IHn in H. inversion H as [m H0]. ∃ m. destruct H0.
split. rewrite H0. apply le_S; apply le_n. assumption.
Qed.
Lemma set_rel_clos_power : ∀ x a1 a2,
set_rel_clos_refl_trans x a1 a2 = true ↔
∃ m, set_rel_power m x a1 a2 = true.
Proof.
unfold set_rel_clos_refl_trans. split; intros.
- apply set_rel_clos_power_aux in H. destruct H as [m H].
∃ m. apply H.
- destruct H as [m H].
apply set_rel_power_size in H; try assumption.
destruct H as [n [H H0]].
apply (set_rel_power_clos_le n); assumption.
Qed.
Lemma set_rel_carrier :
(∀ a1 a2, d a1 a2 → r a1 a2 = true) →
∀ x,
(∀ a1 a2, r a1 a2 = true → set_In a1 x ∧ set_In a2 x) →
∀ a1 a2, set_In a1 x → clos_refl_trans A d a1 a2 →
set_In a2 x.
Proof.
intros. induction H2.
- apply H in H2. apply H0 in H2. apply H2.
- assumption.
- apply IHclos_refl_trans2. apply IHclos_refl_trans1. assumption.
Qed.
Lemma relation_set_rel_clos :
(∀ a1 a2, d a1 a2 → r a1 a2 = true) →
∀ x,
(∀ a1 a2, r a1 a2 = true → set_In a1 x ∧ set_In a2 x) →
∀ a1 a2, set_In a1 x → set_In a2 x → clos_refl_trans A d a1 a2 →
set_rel_clos_refl_trans x a1 a2 = true.
Proof.
intros.
induction H3.
- apply H in H3.
apply set_rel_clos_power; try assumption. ∃ 1.
simpl. apply negb_true_iff. apply set_not_empty_In.
∃ y. apply set_filter_In. rewrite andb_true_iff. repeat split.
assumption. apply H3; assumption.
destruct (DS_decide y y). reflexivity. contradiction n; reflexivity.
- apply set_rel_clos_power; try assumption.
∃ 0. simpl.
destruct (DS_decide x0 x0). reflexivity. contradiction n; reflexivity.
- apply set_rel_carrier with (x:=x) in H3_; try assumption.
assert (set_rel_clos_refl_trans x x0 y = true).
{ apply IHclos_refl_trans1; assumption. }
assert (set_rel_clos_refl_trans x y z = true).
{ apply IHclos_refl_trans2; assumption. }
apply set_rel_clos_power in H3; try assumption.
apply set_rel_clos_power in H4; try assumption.
inversion H3 as [m H5]. inversion H4 as [n H6].
apply set_rel_clos_power; try assumption.
∃ (m+n). apply set_rel_power_add with (a2:=y); assumption.
Qed.
Lemma set_rel_carrier_stable :
∀ x,
set_stable x →
∀ a1 a2, set_In a2 x → clos_refl_trans A d a1 a2 →
set_In a1 x.
Proof.
intros. induction H1.
- apply H in H1; assumption.
- assumption.
- apply IHclos_refl_trans1. apply IHclos_refl_trans2. assumption.
Qed.
Lemma relation_set_rel_clos_stable :
(∀ a1 a2, d a1 a2 → r a1 a2 = true) →
∀ x,
set_stable x →
∀ a1 a2, set_In a1 x → set_In a2 x → clos_refl_trans A d a1 a2 →
set_rel_clos_refl_trans x a1 a2 = true.
Proof.
intros. induction H3.
- apply set_rel_clos_power; try assumption. ∃ 1.
simpl. apply negb_true_iff. apply set_not_empty_In.
∃ y. apply set_filter_In. rewrite andb_true_iff. repeat split.
assumption. apply H; assumption.
destruct (DS_decide y y). reflexivity. contradiction n; reflexivity.
- apply set_rel_clos_power; try assumption.
∃ 0. simpl.
destruct (DS_decide x0 x0). reflexivity. contradiction n; reflexivity.
- apply set_rel_carrier_stable with (x:=x) in H3_0; try assumption.
assert (set_rel_clos_refl_trans x x0 y = true).
{ apply IHclos_refl_trans1; assumption. }
assert (set_rel_clos_refl_trans x y z = true).
{ apply IHclos_refl_trans2; assumption. }
apply set_rel_clos_power in H3; try assumption.
apply set_rel_clos_power in H4; try assumption.
inversion H3 as [m H5]. inversion H4 as [n H6].
apply set_rel_clos_power; try assumption.
∃ (m+n). apply set_rel_power_add with (a2:=y); assumption.
Qed.
Lemma set_rel_clos_relation_iff :
(∀ a1 a2, d a1 a2 ↔ r a1 a2 = true) →
∀ x,
(∀ a1 a2, d a1 a2 → set_In a1 x ∧ set_In a2 x) →
∀ a1 a2, set_In a1 x → set_In a2 x →
(clos_refl_trans A d a1 a2 ↔ set_rel_clos_refl_trans x a1 a2 = true).
Proof.
split; intros.
- apply relation_set_rel_clos; try assumption.
apply H. intros; apply H0; apply H; assumption.
- apply set_rel_clos_relation with (x:=x); try assumption.
apply H.
Qed.
Lemma set_rel_clos_relation_stable_iff :
(∀ a1 a2, d a1 a2 ↔ r a1 a2 = true) →
∀ x,
set_stable x →
∀ a1 a2, set_In a1 x → set_In a2 x →
(clos_refl_trans A d a1 a2 ↔ set_rel_clos_refl_trans x a1 a2 = true).
Proof.
split; intros.
- apply relation_set_rel_clos_stable; try assumption.
apply H.
- apply set_rel_clos_relation with (x:=x); try assumption.
apply H.
Qed.
End relation.
Lemma set_rel_clos_refl_trans_inverse_stable :
∀ `{DS:DecidableType} d r x y,
(∀ a1 a2, d a1 a2 ↔ r a1 a2 = true) →
y \subseteq x →
set_stable d x →
set_stable d (set_inverse (set_rel_clos_refl_trans r x) x y).
Proof.
intros.
unfold set_stable; intros.
apply set_inverse_r in H2.
apply set_inverse_r.
destruct H2. inversion H4 as [l'' [H5 H6]].
assert (set_In l x).
{ unfold set_stable in H1. apply H1 with (l':=l'); assumption. }
assert (set_In l'' x). { apply H0; assumption. }
split.
- assumption.
- ∃ l''. split. assumption.
apply set_rel_clos_power in H6; try assumption.
apply set_rel_clos_power; try assumption.
inversion H6 as [m H9]. ∃ (S m).
apply set_rel_power_add with (n:=1) (a2:=l').
simpl. apply negb_true_iff. apply set_not_empty_In. ∃ l'.
apply set_filter_In. rewrite andb_true_iff. repeat split. assumption.
apply H; assumption.
destruct (DS_decide l' l'). reflexivity. contradiction n; reflexivity.
assumption.
Qed.
Section test.
Context `{DS:DecidableType} (d:relation A).
Context (rl:set(A×A)).
Definition getLabel := set_map fst rl \cup set_map snd rl.
Definition ante_diff x y :=
set_map fst (set_filter (fun aa : A × A ⇒ (snd aa \in? x) &&
(negb (fst aa \in? y))) rl).
Fixpoint aux5 n tt res :=
match n with
| 0 ⇒ tt \cup res
| S n' ⇒ let res' := tt \cup res in
let tt' := ante_diff tt res' in
if set_test_empty tt' then res'
else aux5 n' tt' res'
end.
Functional Scheme aux5_ind := Induction for aux5 Sort Prop.
Lemma ante_diff_In : ∀ x y a, a \in ante_diff x y ↔
¬ a \in y ∧ ∃ a', a' \in x ∧ (a, a') \in rl.
Proof.
intros. unfold ante_diff. rewrite set_map_In. split; intros.
- destruct H as [(a0, a1) [H H0]]. simpl in H0; subst a0.
rewrite set_filter_In in H. rewrite andb_true_iff in H.
rewrite set_mem_correct_iff in H. decompose [and] H; clear H.
simpl in H2, H3. rewrite negb_true_iff in H3. rewrite set_mem_complete_iff in H3.
split; try assumption.
∃ a1. split; assumption.
- destruct H as [H [a' [H0 H1]]].
∃ (a,a'). split; try reflexivity. rewrite set_filter_In.
rewrite andb_true_iff. rewrite set_mem_correct_iff. rewrite negb_true_iff.
rewrite set_mem_complete_iff. repeat split; assumption.
Qed.
Global Add Parametric Morphism : ante_diff
with signature set_same ==> set_same ==> set_same as set_same_ante_diff.
Proof.
intros. apply set_same_In_iff; intros.
rewrite 2!ante_diff_In.
split; intros.
- destruct H1 as [H1 [a' [H2 H3]]]. split. rewrite <- H0. assumption.
∃ a'. rewrite <- H. split; assumption.
- destruct H1 as [H1 [a' [H2 H3]]]. split. rewrite H0. assumption.
∃ a'. rewrite H. split; assumption.
Qed.
Global Add Parametric Morphism : aux5
with signature eq ==> set_same ==> set_same ==> set_same as set_same_aux5.
Proof.
intros y x y0 H x0. revert y0 H. functional induction (aux5 y x x0); intros.
- simpl. rewrite H, H0. reflexivity.
- simpl. rewrite H, H0 in e0. rewrite e0.
rewrite H, H0. reflexivity.
- simpl. rewrite H, H0 in e0. rewrite e0. apply IHs.
+ rewrite H, H0. reflexivity.
+ rewrite H, H0. reflexivity.
Qed.
Lemma ante_diff_emptyset_l : ∀ y, ante_diff \emptyset y \equiv \emptyset.
Proof.
intros. unfold set_same, set_incl; split; intros.
- rewrite ante_diff_In in H. destruct H as [H [a' [H0 H1]]]. inversion H0.
- inversion H.
Qed.
Lemma aux5_equation_S : ∀ n tt res,
aux5 (S n) tt res \equiv aux5 n (ante_diff tt (tt \cup res)) (tt \cup res).
Proof.
intros. simpl. destruct (set_test_empty _) eqn:Heqempty; try reflexivity.
rewrite set_test_empty_correct in Heqempty. rewrite Heqempty. destruct n.
simpl. rewrite set_same_union_empty_l. reflexivity. simpl.
rewrite ante_diff_emptyset_l. replace (set_test_empty \emptyset) with true by reflexivity.
rewrite set_same_union_empty_l. reflexivity.
Qed.
Lemma aux5_incl_res : ∀ n tt res, tt \cup res \subseteq aux5 n tt res.
Proof.
intros n. induction n; intros.
- simpl. apply set_incl_refl.
- rewrite aux5_equation_S.
apply set_incl_trans with (y:=ante_diff tt (tt \cup res) \cup tt \cup res).
unfold set_incl; intros. rewrite set_union_In. right; assumption.
apply IHn.
Qed.
Lemma aux5_grow : ∀ m tt res n, m ≤ n → set_incl (aux5 m tt res) (aux5 n tt res).
Proof.
intros m. induction m; intros.
- simpl. apply aux5_incl_res.
- destruct n; [ inversion H |].
rewrite 2!aux5_equation_S.
apply IHm. apply le_S_n in H; assumption.
Qed.
Lemma set_rel_power_incl : ∀ (r1 r2 : A → A → bool) n x,
(∀ a b, r1 a b = true → r2 a b = true) →
∀ a b, set_rel_power r1 n x a b = true → set_rel_power r2 n x a b = true.
Proof.
intros r1 r2 n x H. induction n; intros.
- simpl in H0. simpl. assumption.
- simpl in H0. simpl. rewrite negb_true_iff in ×. rewrite set_not_empty_In in H0.
rewrite set_not_empty_In. destruct H0 as [a' H0].
∃ a'. rewrite set_filter_In in H0. rewrite set_filter_In. destruct H0.
split; try assumption. rewrite andb_true_iff in ×.
destruct H1. split.
+ apply H; assumption.
+ apply IHn; assumption.
Qed.
Fixpoint first {A} (f:A → bool) (l:list A) :=
match l with
| [] ⇒ 0
| a :: l' ⇒ if f a then 0 else S (first f l')
end.
Lemma first_false : ∀ {A} (f:A → bool) (l:list A) n,
n < first f l → ∀ a, f a = false → f (nth n l a) = false.
Proof.
intros. revert l H. induction n; intros.
- destruct l. simpl. assumption. simpl. simpl in H. destruct (f a0).
inversion H. reflexivity.
- destruct l. simpl. assumption. simpl. apply IHn.
simpl in H. destruct (f a0). inversion H. apply le_S_n in H; assumption.
Qed.
Lemma first_false_forall : ∀ {A} (f:A → bool) (l:list A),
Forall (fun a ⇒ f a = false) (firstn (first f l) l).
Proof.
intros. induction l.
- constructor.
- simpl. destruct (f a) eqn:Heqf. constructor.
simpl. constructor; assumption.
Qed.
Lemma first_true : ∀ {A} (f:A → bool) (l:list A),
∀ a, f a = true → f (nth (first f l) l a) = true.
Proof.
intros. induction l.
- simpl. assumption.
- simpl. destruct (f a0) eqn:Heqf. assumption. apply IHl.
Qed.
Lemma first_true_if : ∀ {A} (f:A → bool) (l:list A) a,
first f l < length l → f (nth (first f l) l a) = true.
Proof.
intros.
induction l. inversion H.
simpl first. destruct (f a0) eqn:Heqf. simpl. assumption.
simpl. apply IHl. simpl in H. rewrite Heqf in H. apply le_S_n in H; assumption.
Qed.
Lemma nth_not_default : ∀ {A} (l:list A) n,
n < length l → ∀ a b, nth n l a = nth n l b.
Proof.
intros. revert l H. induction n; intros. destruct l. inversion H. reflexivity.
destruct l. inversion H. simpl. apply IHn. simpl in H.
apply le_S_n in H; assumption.
Qed.
Lemma firstn_incl : ∀ {A} (l:list A) n a,
In a (firstn n l) → In a l.
Proof.
intros. revert l H. induction n; intros.
- simpl in H. inversion H.
- destruct l. simpl in H. inversion H. simpl in H.
simpl. destruct H. left; assumption. right. apply IHn; assumption.
Qed.
Lemma forall_sorted : ∀ {A} (l:list A) f,
Forall f l → Sorted (fun a a' ⇒ f a) l.
Proof.
intros. induction H.
constructor.
constructor. apply IHForall.
destruct l. constructor. constructor. assumption.
Qed.
Lemma forall_sorted_firstn : ∀ {A} (l:list A) f n,
Forall f (firstn n l) → Sorted (fun a a' ⇒ f a) (firstn (S n) l).
Proof.
intros. revert l H. induction n; intros.
destruct l.
constructor. simpl. constructor. constructor. constructor.
destruct l.
constructor.
remember (S n) as m. simpl. subst m. inversion H. constructor.
apply IHn. assumption. destruct l. constructor. constructor. assumption.
Qed.
Lemma sorted_combine : ∀ {A} (l:list A) f1 f2,
Sorted f1 l → Sorted f2 l → Sorted (fun a a' ⇒ f1 a a' ∧ f2 a a') l.
Proof.
intros. induction l.
- constructor.
- inversion H. inversion H0.
constructor. apply IHl; assumption.
destruct l. constructor. constructor. inversion H4. inversion H8.
split; assumption.
Qed.
Lemma Is_true_eq_true_iff : ∀ b, Is_true b ↔ b = true.
Proof.
split; intros.
apply Is_true_eq_true. assumption.
apply Is_true_eq_left. assumption.
Qed.
Lemma hdrel_fun_ext : ∀ {A} (l:list A) f1 f2,
(∀ x y, f1 x y ↔ f2 x y) → ∀ a,
(HdRel f1 a l ↔ HdRel f2 a l).
Proof.
split; intros.
- inversion H0.
+ constructor.
+ constructor. rewrite <- H. assumption.
- inversion H0.
+ constructor.
+ constructor. rewrite H. assumption.
Qed.
Lemma sorted_fun_ext : ∀ {A} (l:list A) f1 f2,
(∀ x y, f1 x y ↔ f2 x y) →
(Sorted f1 l ↔ Sorted f2 l).
Proof.
split; intros.
- induction H0.
+ constructor.
+ constructor. assumption. rewrite <- (hdrel_fun_ext _ f1); assumption.
- induction H0.
+ constructor.
+ constructor. assumption. rewrite (hdrel_fun_ext _ _ f2); assumption.
Qed.
Lemma hdrel_firstn : ∀ {A} (l:list A) f a,
HdRel f a l →
∀ n, HdRel f a (firstn n l).
Proof.
intros. destruct n; intros.
- simpl. constructor.
- destruct l. constructor. simpl. constructor. inversion H. assumption.
Qed.
Lemma forall_firstn : ∀ {A} (l:list A) f,
Forall f l →
∀ n, Forall f (firstn n l).
Proof.
intros. apply Forall_forall. rewrite Forall_forall in H.
intros. apply H. apply firstn_incl in H0. assumption.
Qed.
Lemma sorted_firstn : ∀ {A} (l:list A) f,
Sorted f l →
∀ n, Sorted f (firstn n l).
Proof.
intros. revert l H. induction n; intros.
- simpl. constructor.
- destruct l. simpl. constructor.
simpl. inversion H. constructor. apply IHn. assumption.
apply hdrel_firstn. assumption.
Qed.
Lemma forall_fun_ext : ∀ {A} (l:list A) f1 f2,
(∀ a, f1 a ↔ f2 a) →
(Forall f1 l ↔ Forall f2 l).
Proof.
split; intros.
- induction H0.
+ constructor.
+ constructor. rewrite <- H. assumption. assumption.
- induction H0.
+ constructor.
+ constructor. rewrite H. assumption. assumption.
Qed.
Lemma firstn_full : ∀ {A} (l:list A) n,
length l ≤ n → firstn n l = l.
Proof.
intros A0 l. induction l; intros.
- destruct n; reflexivity.
- destruct n. inversion H. simpl. rewrite IHl. reflexivity.
simpl in H.
apply le_S_n in H. assumption.
Qed.
Lemma aux5_correct : ∀ n x y a, a \in aux5 n x y ↔ a \in y ∨
∃ a', a' \in x ∧
set_rel_clos_refl_trans_aux
(fun t t' ⇒ ((t, t') \in? rl) && (negb (t \in? y))) n getLabel a a' = true.
Proof.
intros n. induction n; intros.
- simpl. split; intros.
+ destruct (set_In_dec a y).
× left; assumption.
× rewrite set_union_In in H. destruct H; [| contradiction]. right.
∃ a. split; try assumption. destruct (DS_decide a a).
reflexivity. contradiction n0; reflexivity.
+ destruct H.
× rewrite set_union_In. right; assumption.
× destruct H as [a' [H H0]]. destruct (DS_decide a a'). subst a'.
rewrite set_union_In. left; assumption. discriminate H0.
- split; intros.
+ rewrite aux5_equation_S in H. apply IHn in H. destruct H.
× rewrite set_union_In in H. { destruct H.
- right. ∃ a. split; try assumption.
apply set_rel_power_clos_le with (m:=0).
apply le_0_n. simpl. destruct (DS_decide a a). reflexivity.
contradiction n0; reflexivity.
- left; assumption. }
× destruct H as [a' [H H0]].
apply ante_diff_In in H. destruct H as [H1 [a'' [H2 H3]]].
apply set_rel_clos_power_aux in H0. destruct H0 as [m [H4 H5]].
right. ∃ a''. split; try assumption.
apply (set_rel_power_clos_le _ (S m)). apply le_n_S; assumption.
replace (S m) with (m + 1) by (rewrite Nat.add_comm; reflexivity).
apply (set_rel_power_add _ _ _ a').
apply set_rel_power_incl with (r1:=fun t t' : A ⇒ ((t, t') ∈? rl) && negb (t ∈? x ∪ y)).
intros. rewrite andb_true_iff in H. rewrite andb_true_iff. destruct H.
split; try assumption. rewrite negb_true_iff in ×. rewrite set_mem_complete_iff in H0.
rewrite set_mem_complete_iff. intros contra. apply H0. apply set_union_In. right; assumption.
assumption.
simpl. rewrite negb_true_iff. rewrite set_not_empty_In.
∃ a''. rewrite set_filter_In. rewrite andb_true_iff.
rewrite andb_true_iff.
rewrite set_mem_correct_iff. { repeat split.
- unfold getLabel. rewrite set_union_In. right. rewrite set_map_In.
∃ (a', a''). split; try reflexivity. assumption.
- assumption.
- rewrite negb_true_iff. rewrite set_mem_complete_iff.
intros contra. apply H1. rewrite set_union_In. right; assumption.
- destruct (DS_decide a'' a''). reflexivity. contradiction n0. reflexivity. }
+ destruct H.
× rewrite aux5_equation_S. apply IHn.
left. rewrite set_union_In. right; assumption.
× destruct H as [a' [H H0]]. apply set_rel_clos_power_aux in H0.
destruct H0 as [m [H0 H1]]. { destruct m.
- simpl in H1. destruct (DS_decide a a'). subst a'.
rewrite aux5_equation_S. apply IHn. left.
rewrite set_union_In. left; assumption.
discriminate H1.
- apply le_S_n in H0.
assert (a \in getLabel) as Ha.
{ replace (S m) with (1+m) in H1 by reflexivity. apply set_rel_add_power in H1.
destruct H1 as [a'' [H2 H3]]. simpl in H2.
rewrite negb_true_iff in H2. rewrite set_not_empty_In in H2. destruct H2 as [a0 H2].
rewrite set_filter_In in H2. rewrite 2!andb_true_iff in H2. rewrite set_mem_correct_iff in H2.
decompose [and] H2; clear H2.
unfold getLabel. rewrite set_union_In. left. rewrite set_map_In.
∃ (a, a0). split; try reflexivity. assumption.
}
replace (S m) with (m + 1) in H1 by (rewrite Nat.add_comm; reflexivity).
apply set_rel_add_power in H1. destruct H1 as [a'' [H1 H2]].
simpl in H2. rewrite negb_true_iff in H2. rewrite set_not_empty_In in H2.
destruct H2 as [a0 H2]. rewrite set_filter_In in H2. rewrite andb_true_iff in H2.
rewrite andb_true_iff in H2.
rewrite set_mem_correct_iff in H2.
rewrite negb_true_iff in H2. rewrite set_mem_complete_iff in H2.
decompose [and] H2; clear H2.
destruct (DS_decide a0 a'); [| discriminate H6]; clear H6. subst a0.
assert (a'' \in getLabel) as Ha2.
{ unfold getLabel. rewrite set_union_In. left. rewrite set_map_In.
∃ (a'', a'). split; try reflexivity. assumption.
}
apply set_rel_power_list in H1; try assumption.
decompose_ex H1. decompose [and] H1; clear H1.
destruct (Nat.lt_ge_cases (first (fun t ⇒ t \in? x) l) (S m)).
+ assert(set_rel_power (fun t t' : A ⇒ ((t, t') ∈? rl) && negb (t ∈? x \cup y))
(first (fun t ⇒ t \in? x) l) getLabel a (nth (first (fun t ⇒ t \in? x) l) l a) = true).
{ apply (set_list_rel_power _ _ _ _ _ (firstn (S (first (fun t ⇒ t \in? x) l)) l)).
- rewrite firstn_length. apply Nat.min_l_iff. rewrite H2. assumption.
- destruct l. discriminate H2. simpl in H6. subst a0. simpl. reflexivity.
- rewrite last_firstn. apply nth_not_default.
rewrite H2. assumption. rewrite H2. assumption.
- apply forall_firstn. assumption.
- rewrite sorted_fun_ext
with (f2:=fun a a' : A ⇒
Is_true (((a, a') ∈? rl) && negb (a ∈? y)) ∧ ¬ a \in x).
apply sorted_combine. apply sorted_firstn. assumption.
apply forall_sorted_firstn.
apply Forall_impl with (P:=fun a0 ⇒ (a0 \in? x) = false).
intros. apply set_mem_complete_iff. assumption.
apply first_false_forall.
intros. rewrite 2!Is_true_eq_true_iff. rewrite 2!andb_true_iff.
rewrite 2!negb_true_iff. rewrite 2!set_mem_complete_iff.
rewrite set_union_In. rewrite decidable.not_or_iff.
rewrite and_assoc. rewrite (and_comm (¬ x0 \in y)). reflexivity.
}
apply (aux5_grow n). apply le_S; apply le_n.
apply IHn. right. ∃ (nth (first (fun t : A ⇒ t ∈? x) l) l a).
split.
× rewrite <- set_mem_correct_iff.
apply (first_true_if (fun t ⇒ t \in? x)). rewrite H2. assumption.
× { apply (set_rel_power_clos_le _ (first (fun t : A ⇒ t ∈? x) l)).
- apply le_S_n in H1. rewrite H1. assumption.
- apply set_rel_power_incl
with (r1:=fun t t' : A ⇒ ((t, t') ∈? rl) && negb (t ∈? x ∪ y)).
+ intros. rewrite andb_true_iff in H11. rewrite andb_true_iff.
destruct H11. split; try assumption. rewrite negb_true_iff in ×.
rewrite set_mem_complete_iff in H12.
rewrite set_mem_complete_iff. intros contra. apply H12.
apply set_union_In. right; assumption.
+ assumption. }
+ rewrite aux5_equation_S. apply IHn. right.
∃ a''. split.
× rewrite ante_diff_In. { split.
- intros contra. rewrite set_union_In in contra.
destruct contra; [| contradiction].
pose proof (first_false_forall (fun t ⇒ t \in? x) l).
rewrite Forall_forall in H11. specialize (H11 a'').
rewrite firstn_full in H11.
+ rewrite set_mem_complete_iff in H11. apply H11; try assumption.
rewrite <- H5. apply last_not_empty_In. destruct l. discriminate H2.
discriminate.
+ rewrite H2. assumption.
- ∃ a'. split; assumption. }
× apply (set_rel_power_clos_le _ m); try assumption.
apply (set_list_rel_power _ _ _ _ _ l); try assumption.
{ rewrite sorted_fun_ext
with (f2:=fun a a' : A ⇒
Is_true (((a, a') ∈? rl) && negb (a ∈? y)) ∧ ¬ a \in x).
- apply sorted_combine; try assumption.
apply forall_sorted.
apply Forall_impl with (P:=fun a0 ⇒ (a0 \in? x) = false).
+ intros. apply set_mem_complete_iff. assumption.
+ rewrite <- (firstn_full _ (first (fun t : A ⇒ t ∈? x) l)).
× apply first_false_forall.
× rewrite H2. assumption.
- intros. rewrite 2!Is_true_eq_true_iff. rewrite 2!andb_true_iff.
rewrite 2!negb_true_iff. rewrite 2!set_mem_complete_iff.
rewrite set_union_In. rewrite decidable.not_or_iff.
rewrite and_assoc. rewrite (and_comm (¬ x0 \in y)). reflexivity. } }
Qed.
Definition set_refl_trans_inverse_aux n (x:set A) := aux5 n x \emptyset.
Lemma set_refl_trans_inverse_aux_correct :
∀ n x a, a \in set_refl_trans_inverse_aux n x ↔
∃ a', a' \in x ∧
set_rel_clos_refl_trans_aux
(fun t t' ⇒ ((t, t') \in? rl)) n getLabel a a' = true.
Proof.
intros. unfold set_refl_trans_inverse_aux.
rewrite aux5_correct. split; intros.
- destruct H; [ inversion H |]. destruct H as [a' [H H0]].
∃ a'. split; try assumption.
apply set_rel_clos_power_aux in H0. destruct H0 as [m [H0 H1]].
apply (set_rel_power_clos_le _ m); try assumption.
apply set_rel_power_incl with (r1:=fun t t' ⇒ ((t, t') ∈? rl) && negb (t ∈? ∅));
try assumption.
intros. rewrite andb_true_iff in H2. apply H2.
- right. destruct H as [a' [H H0]].
∃ a'. split; try assumption.
apply set_rel_clos_power_aux in H0. destruct H0 as [m [H0 H1]].
apply (set_rel_power_clos_le _ m); try assumption.
apply set_rel_power_incl with (r1:=fun t t' ⇒ ((t, t') ∈? rl));
try assumption.
intros. rewrite andb_true_iff. split. assumption.
rewrite negb_true_iff. rewrite set_mem_complete_iff. intros contra.
inversion contra.
Qed.
Definition set_refl_trans_inverse (x:set A) :=
set_refl_trans_inverse_aux (set_size getLabel) x.
Lemma set_refl_trans_inverse_correct :
∀ x a, a \in set_refl_trans_inverse x ↔
∃ a', a' \in x ∧
set_rel_clos_refl_trans
(fun t t' ⇒ ((t, t') \in? rl)) getLabel a a' = true.
Proof.
intros.
unfold set_refl_trans_inverse.
rewrite set_refl_trans_inverse_aux_correct.
reflexivity.
Qed.
Lemma set_refl_trans_inverse_stable :
∀ x a, a \in set_refl_trans_inverse x → a \in getLabel \cup x.
Proof.
intros. rewrite set_refl_trans_inverse_correct in H.
destruct H as [a' [H H0]]. unfold set_rel_clos_refl_trans in H0.
apply set_rel_clos_power_aux in H0. destruct H0 as [m [H0 H1]].
destruct m.
- simpl in H1. destruct (DS_decide a a').
+ subst a'. rewrite set_union_In. right; assumption.
+ discriminate H1.
- replace (S m) with (1 + m) in H1 by reflexivity.
apply set_rel_add_power in H1.
destruct H1 as [a'' [H1 H2]].
+ simpl in H1. rewrite negb_true_iff in H1.
rewrite set_not_empty_In in H1. destruct H1 as [a0 H1].
rewrite set_filter_In in H1. rewrite andb_true_iff in H1.
rewrite set_mem_correct_iff in H1. decompose [and] H1; clear H1.
rewrite set_union_In. left. unfold getLabel.
rewrite set_union_In. left. rewrite set_map_In.
∃ (a, a0). split; try reflexivity. assumption.
Qed.
Lemma relation_set_rel_clos_stable2 :
(∀ a1 a2, d a1 a2 → (a1, a2) \in rl) →
∀ x,
∀ a1 a2, a2 \in x →
clos_refl_trans A d a1 a2 →
a1 \in set_refl_trans_inverse x.
Proof.
intros. rewrite set_refl_trans_inverse_correct.
∃ a2. split; try assumption.
destruct (set_In_dec a2 getLabel).
- assert (set_stable d getLabel).
{ unfold set_stable; intros. apply H in H3.
unfold getLabel. rewrite set_union_In. left. rewrite set_map_In.
∃ (l, l'). split; try reflexivity. assumption.
}
apply (relation_set_rel_clos_stable d); try assumption.
+ intros. rewrite set_mem_correct_iff. apply H; assumption.
+ apply (set_rel_carrier_stable d _ H2 _ a2); assumption.
- apply set_rel_clos_power. ∃ 0. simpl. destruct (DS_decide a1 a2).
reflexivity. contradiction n0. clear H0 n0.
induction H1.
+ apply H in H0. contradiction n.
unfold getLabel. rewrite set_union_In. right.
rewrite set_map_In. ∃ (x0, y). split; try reflexivity.
assumption.
+ reflexivity.
+ specialize (IHclos_refl_trans2 n). subst y. apply IHclos_refl_trans1 in n.
assumption.
Qed.
Lemma set_rel_clos_relation2 :
(∀ a1 a2, (a1, a2) \in rl → d a1 a2) →
∀ x a1,
a1 \in set_refl_trans_inverse x →
∃ a2, a2 \in x ∧ clos_refl_trans A d a1 a2.
Proof.
intros. apply set_refl_trans_inverse_correct in H0.
destruct H0 as [a' [H0 H1]]. ∃ a'. split; try assumption.
apply (set_rel_clos_relation d) in H1. assumption.
intros. rewrite set_mem_correct_iff in H2. apply H; assumption.
Qed.
Lemma set_rel_clos_relation_stable_iff2 :
(∀ a1 a2, (a1, a2) \in rl ↔ d a1 a2) →
∀ x a1, a1 \in set_refl_trans_inverse x ↔ ∃ a2, a2 \in x ∧
clos_refl_trans A d a1 a2.
Proof.
split; intros.
- apply set_rel_clos_relation2 in H0. assumption. apply H.
- destruct H0 as [a2 [H0 H1]].
apply relation_set_rel_clos_stable2 with (a2:=a2); try assumption.
apply H.
Qed.
Lemma set_incl_emptyset_l : ∀ x, \emptyset \subseteq x.
Proof.
intros; unfold set_incl; intros. inversion H.
Defined.
End test.
Lemma set_rel_clos_refl_trans_inverse_stable2 :
∀ `{DS:DecidableType} d rl x,
(∀ a1 a2, (a1, a2) \in rl ↔ d a1 a2) →
set_stable d (set_refl_trans_inverse rl x).
Proof.
intros.
unfold set_stable; intros.
apply (set_rel_clos_relation_stable_iff2 d _ H).
apply (set_rel_clos_relation_stable_iff2 d _ H) in H0.
destruct H0 as [a2 [H2 H3]].
∃ a2. split; try assumption. apply rt_trans with (y:=l').
apply rt_step. assumption. assumption.
Qed.