Tmp.v

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.