Created
March 30, 2023 10:53
-
-
Save mukeshtiwari/4bda631fb74562b197a074358eb53a0f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Notation "a =S= b" := (brel_set (brel_product eqA eqP) a b = true) (at level 70). | |
(* = or =S=, both are fine! *) | |
Lemma iterate_minset_inv_2 : | |
forall (X W Y : finite_set (A * P)) au bu, | |
find (theory.below (manger_pre_order lteA) (au, bu)) X = None -> | |
find (theory.below (manger_pre_order lteA) (au, bu)) Y = None -> | |
(* | |
(∀ t : A * P, | |
in_set (brel_product eqA eqP) X t = true -> | |
theory.below (manger_pre_order lteA) (au, bu) t = false) -> | |
*) | |
snd (iterate_minset (manger_pre_order lteA) W ((au, bu) :: Y) X) = | |
(au, bu) :: snd (iterate_minset (manger_pre_order lteA) W Y X). | |
Proof. | |
induction X as [|(ax, bx) X IHx]. | |
+ | |
intros * Ha Hw. | |
cbn; reflexivity. | |
+ | |
intros * Ha Hw. | |
cbn in Ha |- . | |
destruct (theory.below (manger_pre_order lteA) (au, bu) (ax, bx)); | |
[congruence |]. | |
(* From Ha, we know that there is nothing strictly below (au, bu) in X *) | |
pose proof find_below_none (A * P) | |
(brel_product eqA eqP) refAP symAP | |
(manger_pre_order lteA) | |
cong_manger_preorder X _ Ha as Hb. | |
(* Hb is the proof that there is nothing below (au, bu) *) | |
cbn. | |
destruct (find (theory.below (manger_pre_order lteA) (ax, bx)) X) | |
as [(pa, pb) |] eqn:Hc. | |
++ | |
eapply IHx. | |
admit. | |
admit. | |
++ | |
unfold manger_pre_order, | |
brel_product, brel_trivial, | |
theory.below, and.bop_and. | |
(* From Hc, I know that there is nothign | |
below (ax, bx) *) | |
pose proof find_below_none (A * P) | |
(brel_product eqA eqP) refAP symAP | |
(manger_pre_order lteA) | |
cong_manger_preorder X _ Hc as Hd. | |
destruct (theory.below (manger_pre_order lteA) (ax, bx) (au, bu)) | |
eqn:He. | |
Admitted. | |
Lemma axiom_on_lteA_true : | |
forall a au ap, | |
eqA au a = true -> | |
lteA ap au = true -> | |
lteA ap a = true. | |
Admitted. | |
Lemma axiom_on_lteA_false : | |
forall a au ap, | |
eqA au a = true -> | |
lteA au ap = false -> | |
lteA a ap = false. | |
Admitted. | |
Lemma theory_below_cong : | |
forall t (au a : A) (bu : P), | |
eqA au a = true -> | |
theory.below (manger_pre_order lteA) (au, bu) t = false -> | |
theory.below (manger_pre_order lteA) (a, bu) t = false. | |
Proof. | |
intros (ta, tb) * Ha Hb. | |
eapply theory.below_false_elim in Hb. | |
eapply theory.below_false_intro. | |
destruct Hb as [Hb | Hb]. | |
+ | |
left; | |
unfold manger_pre_order, | |
brel_product, brel_trivial in Hb |- *. | |
rewrite Bool.andb_true_r in Hb |- *. | |
admit. | |
+ | |
right; unfold manger_pre_order, | |
brel_product, brel_trivial in Hb |- *. | |
rewrite Bool.andb_true_r in Hb |- *. | |
admit. | |
Admitted. | |
Fact manger_rewrite_exists : | |
forall (X : finite_set (A * P)) (a : A) p, | |
(∀ t : A * P, | |
in_set (brel_product eqA eqP) X t = true -> | |
theory.below (manger_pre_order lteA) (a, p) t = false) -> | |
exists q : P, in_set (brel_product eqA eqP) X (a, q) = | |
in_set (brel_product eqA eqP) | |
(uop_minset (manger_pre_order lteA) X) (a, q). | |
Admitted. | |
Fact manger_rewrite_forall : | |
forall (X : finite_set (A * P)) (a : A) p, | |
(∀ t : A * P, | |
in_set (brel_product eqA eqP) X t = true -> | |
theory.below (manger_pre_order lteA) (a, p) t = false) -> | |
in_set (brel_product eqA eqP) X (a, p) = true -> | |
in_set (brel_product eqA eqP) | |
(uop_minset (manger_pre_order lteA) X) (a, p) = true. | |
Proof. | |
induction X as [|(ax, bx) X IHx]. | |
+ | |
intros * Ha Hb. | |
cbn in Hb; congruence. | |
+ | |
intros * Ha Hb. | |
cbn in Hb |- *. | |
eapply Bool.orb_true_iff in Hb. | |
destruct Hb as [Hb | Hb]. | |
++ | |
(* from Ha, I know that (ax, bx) is not | |
strictly below (a, p) *) | |
pose proof (Ha (ax, bx)) as Hc; | |
cbn in Hc; rewrite refA, refP in Hc; | |
cbn in Hc; specialize (Hc eq_refl). | |
eapply theory.below_false_elim in Hc. | |
destruct Hc as [Hc | Hc]. | |
* | |
unfold manger_pre_order, | |
brel_product, brel_trivial in Hc. | |
eapply Bool.andb_true_iff in Hb. | |
rewrite Bool.andb_true_r in Hc. | |
destruct Hb as [Hbl Hbr]. | |
(* contradiction *) | |
admit. | |
* | |
unfold manger_pre_order, | |
brel_product, brel_trivial in Hc. | |
eapply Bool.andb_true_iff in Hb. | |
rewrite Bool.andb_true_r in Hc. | |
destruct Hb as [Hbl Hbr]. | |
(* I know that *) | |
assert (Hd : uop_minset (manger_pre_order lteA) ((ax, bx) :: X) = | |
(ax, bx) :: uop_minset (manger_pre_order lteA) X). | |
admit. | |
(* But this is what bothering me. Proving this one | |
is nightmare *) | |
rewrite Hd; cbn; rewrite Hbl, Hbr; | |
cbn; reflexivity. | |
++ | |
(* same reasoning as abouve *) | |
assert (Hd : uop_minset (manger_pre_order lteA) ((ax, bx) :: X) = | |
(ax, bx) :: uop_minset (manger_pre_order lteA) X). | |
admit. | |
rewrite Hd; cbn. | |
(* use induction hypothesis *) | |
assert (He : (∀ t : A * P, | |
in_set (brel_product eqA eqP) X t = true -> | |
theory.below (manger_pre_order lteA) (a, p) t = false)). | |
intros (ta, tb) He. | |
eapply Ha; cbn; rewrite He, | |
Bool.orb_true_r; reflexivity. | |
rewrite (IHx _ _ He Hb), | |
Bool.orb_true_r; reflexivity. | |
Admitted. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment