(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Bitwise operations on nat as list bool *)

Require Import List Omega Bool Setoid.
Require Import utils_tac.

Set Implicit Arguments.

(* Section lb. *)

  Local Reserved Notation "x ⪯ y" (at level 70, no associativity).
  Local Reserved Notation "x ⟂ y" (at level 70, no associativity).
  Local Reserved Notation "x ↓ y" (at level 40, left associativity).
  Local Reserved Notation "x ↑ y" (at level 41, left associativity).

  Local Notation lb := (list bool).
  Local Notation "⟘" := false.
  Local Notation "⟙" := true.
  Local Infix "⪦" := leb (at level 70, no associativity).

  Fact leb_refl : forall x, x ⪦ x.
(* Goal: forall x : bool, leb x x *)
  Proof. intros []; simpl; auto. Qed.

  Fact leb_trans : forall x y z, x ⪦ y -> y ⪦ z -> x ⪦ z.
  Proof. intros [] [] []; simpl; auto. Qed.

  Fact leb_strict : ⟘ ⪦ ⟙.
  Proof. exact I. Qed. 

  Hint Resolve leb_refl leb_trans leb_strict.

  (** We develop the Boolean algebra of lists of Booleans *)

  (* The masking relation *)

  Inductive lb_mask : lb -> lb -> Prop :=
    | in_lb_mask_0 : forall l,                            nil ⪯ l
    | in_lb_mask_1 : forall l,                l ⪯ nil -> ⟘::l ⪯  nil 
    | in_lb_mask_2 : forall x y l m, x ⪦ y -> l ⪯ m   -> x::l ⪯  y::m
  where "l ⪯ m" := (lb_mask l m).

  Fact lb_mask_inv_nil l : ⟘::l ⪯  nil -> l ⪯  nil.
  Proof. inversion 1; auto. Qed. 

  Fact lb_mask_inv_left x l : x::l ⪯  nil -> x = ⟘ /\ l ⪯  nil.
  Proof. inversion 1; auto. Qed. 

  Fact lb_mask_inv_cons x y l m : x::l ⪯ y::m -> leb x y /\ l ⪯  m.
  Proof. inversion 1; tauto. Qed.

  Fact lb_mask_inv_cons_nil l : ⟙::l ⪯ nil -> False.
  Proof. inversion 1. Qed.

  Fact lb_mask_inv_cons_cons l m : ⟙::l ⪯ ⟘::m -> False.
  Proof.
(* Goal: forall _ : lb_mask (@cons bool true l) (@cons bool false m), False *)
    intros H; apply lb_mask_inv_cons, proj1 in H; discriminate.
  Qed.
 
  Definition lb_mask_leb := in_lb_mask_2.

  Fact lb_mask_refl l : l ⪯ l.
  Proof. induction l as [ | [] ]; constructor; simpl; auto. Qed.

  Fact lb_mask_trans l m k : l ⪯ m -> m ⪯ k -> l ⪯ k.
  Proof.
(* Goal: forall (_ : lb_mask l m) (_ : lb_mask m k), lb_mask l k *)
    intros H1; revert H1 k.
(* Goal: forall (_ : lb_mask l m) (k : list bool) (_ : lb_mask m k), lb_mask l k *)
    induction 1 as [ l | l H1 IH1 | x y l m H1 IH1 ].
    + intros; constructor.
    + intros [ | z k ] Hk.
      * constructor; auto.
      * constructor; simpl; auto; apply IH1; constructor.
    + intros [ | z k ] Hk.
      * apply lb_mask_inv_left in Hk; destruct Hk as (? & Hk); subst y.
(* Goal: lb_mask (@cons bool x l) (@nil bool) *)
        destruct x; simpl in H1; try discriminate.
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
        constructor; auto.
      * apply lb_mask_inv_cons in Hk. 
(* Goal: lb_mask (@cons bool x l) (@cons bool z k) *)
        destruct Hk as (H2 & Hk).
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
        constructor; auto.
(* Goal: leb x z *)
        revert x y z H1 H2.
(* Goal: forall (x y v : bool) (_ : leb x y) (_ : or (@eq bool y false) (@eq bool v false)), or (@eq bool x false) (@eq bool v false) *)
        intros [] [] []; simpl; auto.
  Qed.

  Hint Resolve lb_mask_refl lb_mask_trans.

  Definition lb_mask_equiv l m := l ⪯ m /\ m ⪯ l.

  Local Infix "≂" := lb_mask_equiv (at level 70, no associativity).

  Fact lb_mask_equiv_refl l : l ≂ l.
  Proof. split; auto. Qed.

  Fact lb_mask_equiv_sym l m : l ≂ m -> m ≂ l.
  Proof. intros []; split; auto. Qed.

  Fact lb_mask_equiv_trans l m k : l ≂ m -> m ≂ k -> l ≂ k.
  Proof. intros [] []; split; eauto. Qed.

  Hint Resolve in_lb_mask_0 lb_mask_refl lb_mask_equiv_refl.

  Add Parametric Relation: (lb) (lb_mask_equiv)
      reflexivity proved by  lb_mask_equiv_refl
      symmetry proved by     lb_mask_equiv_sym
      transitivity proved by lb_mask_equiv_trans
    as lb_mask_equiv_rst.

  Local Notation lbeq := lb_mask_equiv (only parsing).

  Add Parametric Morphism: (lb_mask) with signature (lbeq) ==> (lbeq) ==> (iff) as lb_mask_le_iff.
  Proof. 
(* Goal: forall (x y : list bool) (_ : lb_mask_equiv x y) (x0 y0 : list bool) (_ : lb_mask_equiv x0 y0), iff (lb_mask x x0) (lb_mask y y0) *)
    intros x1 y1 (H1 & H2) x2 y2 (H3 & H4); split; intros H5.
    + apply lb_mask_trans with (1 := H2), lb_mask_trans with (1 := H5); auto.
    + apply lb_mask_trans with (1 := H1), lb_mask_trans with (1 := H5); auto.
  Qed.

  Add Parametric Morphism: (@cons bool) with signature (eq) ==> (lbeq) ==> (lbeq) as lb_mask_equiv_cons.
  Proof.
(* Goal: forall (y : bool) (x y0 : list bool) (_ : lb_mask_equiv x y0), lb_mask_equiv (@cons bool y x) (@cons bool y y0) *)
    intros [] ? ? []; split; apply lb_mask_leb; simpl; auto.
  Qed.

  Fact lb_mask_app l m a b : length l = length m -> l ⪯ m -> a ⪯ b -> l++a ⪯ m++b.
  Proof.
    revert m; induction l as [ | x l IHl ]; intros [ | y m ]; try discriminate; auto;
      simpl; intros H H1 H2.
(* Goal: lb_mask (@cons bool x (@app bool l a)) (@cons bool y (@app bool m b)) *)
    apply lb_mask_inv_cons in H1; destruct H1 as (H1 & H3).
(* Goal: lb_mask (@cons bool x (@app bool l a)) (@cons bool y (@app bool m b)) *)
    constructor 3; auto.
  Qed.

  Fact lb_mask_equiv_app l m a b : length l = length m -> l ≂ m -> a ≂ b -> l++a ≂ m++b.
  Proof.
(* Goal: forall (_ : @eq nat (@length bool l) (@length bool m)) (_ : lb_mask_equiv l m) (_ : lb_mask_equiv a b), lb_mask_equiv (@app bool l a) (@app bool m b) *)
    intros H (? & ?) (? & ?); split; apply lb_mask_app; auto.
  Qed.

  Inductive lb_ortho : lb -> lb -> Prop :=
    | in_lb_ortho_0 : forall l, nil ⟂ l
    | in_lb_ortho_1 : forall l, l ⟂ nil
    | in_lb_ortho_2 : forall x y l m, (x = ⟘ \/ y = ⟘) -> l ⟂ m -> x::l ⟂ y::m
  where "x ⟂ y" := (lb_ortho x y).

  Hint Constructors lb_ortho.

  Fact lb_ortho_cons_inv x y l m : x::l ⟂ y::m -> (x = ⟘ \/ y = ⟘) /\ l ⟂ m.
  Proof. inversion 1; auto. Qed.

  Fact lb_ortho_anti_left a b x : a ⪯ b -> b ⟂ x -> a ⟂ x.
  Proof.
(* Goal: forall (_ : lb_mask a b) (_ : lb_ortho b x), lb_ortho a x *)
    intros H; revert H x.
    induction 1 as [ l | m H1 IH1 | x y l m H1 H2 IH2  ]; intros z H3; try (constructor; fail);
      destruct z as [ | v z ]; try (constructor; fail).
    + constructor; auto; apply IH1; constructor.
    + apply lb_ortho_cons_inv in H3.
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
      destruct H3 as (H3 & H4).
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
      constructor; auto. 
(* Goal: or (@eq bool x false) (@eq bool v false) *)
      revert x y v H1 H3.
(* Goal: forall (x y v : bool) (_ : leb x y) (_ : or (@eq bool y false) (@eq bool v false)), or (@eq bool x false) (@eq bool v false) *)
      intros [] [] []; simpl; auto.
  Qed.

  Fact lb_ortho_sym a b : a ⟂ b -> b ⟂ a.
  Proof. induction 1; constructor; tauto. Qed.

  Fact lb_ortho_anti a b x y : a ⪯ b -> x ⪯ y -> b ⟂ y -> a ⟂ x.
  Proof. 
(* Goal: forall (_ : lb_mask a b) (_ : lb_mask x y) (_ : lb_ortho b y), lb_ortho a x *)
    intros H1 H2 H3.
    apply lb_ortho_anti_left with (1 := H1), lb_ortho_sym,
          lb_ortho_anti_left with (1 := H2), lb_ortho_sym.
(* Goal: @eq (list bool) (lb_pointwise (@cons bool x l) (@cons bool y m)) (@cons bool (f x y) (lb_pointwise l m)) *)
    trivial.
  Qed.

  Add Parametric Morphism: (lb_ortho) with signature (lbeq) ==> (lbeq) ==> (iff) as lb_ortho_iff.
  Proof. intros ? ? [] ? ? []; split; apply lb_ortho_anti; auto. Qed.

  Section lb_pointwise.

    Variable (f : bool -> bool -> bool).

    Fixpoint lb_pointwise l m := 
      match l, m with
        | nil,   nil  => nil
        |  _,    nil  => map (fun x => f x ⟘) l
        | nil,     _  => map (f ⟘) m
        | x::l, y::m  => f x y :: lb_pointwise l m
      end.

    Fact lb_pointwise_nil : lb_pointwise nil nil = nil.
    Proof. trivial. Qed.

    Fact lb_pointwise_left l : lb_pointwise l nil = map (fun x => f x ⟘) l.
    Proof. destruct l; trivial. Qed.

    Fact lb_pointwise_right l : lb_pointwise nil l = map (f ⟘) l.
    Proof. destruct l; trivial. Qed.
 
    Fact lb_pointwise_cons x l y m : lb_pointwise (x::l) (y::m) = f x y :: lb_pointwise l m.
    Proof. trivial. Qed.

    Fact lb_pointwise_length n l m : length l <= n -> length m <= n -> length (lb_pointwise l m) <= n.
    Proof.
(* Goal: forall (_ : le (@length bool l) n) (_ : le (@length bool m) n), le (@length bool (lb_pointwise l m)) n *)
      revert l m; induction n as [ | n IHn ].
      + intros [] []; simpl; omega.
      + intros [ | x l ] [ | y m ]; simpl; try rewrite map_length; auto.
(* Goal: forall (_ : le (S (@length bool l)) (S n)) (_ : le (S (@length bool m)) (S n)), le (S (@length bool (lb_pointwise l m))) (S n) *)
        intros; apply le_n_S, IHn; omega.
    Qed.

    Fact lb_pointwise_sym l m : (forall x y, f x y = f y x) -> lb_pointwise l m = lb_pointwise m l.
    Proof.
(* Goal: forall _ : forall x y : bool, @eq bool (f x y) (f y x), @eq (list bool) (lb_pointwise l m) (lb_pointwise m l) *)
      intros H; revert l m; induction l as [ | x l IHl ]; intros m.
      + rewrite lb_pointwise_left, lb_pointwise_right.
(* Goal: @eq (list bool) (@map bool bool (fun x : bool => f x false) (@cons bool x l)) (@map bool bool (f false) (@cons bool x l)) *)
        apply map_ext; intro; auto.
      + destruct m as [ | y m ].
        * rewrite lb_pointwise_left, lb_pointwise_right.
(* Goal: @eq (list bool) (@map bool bool (fun x : bool => f x false) (@cons bool x l)) (@map bool bool (f false) (@cons bool x l)) *)
          apply map_ext; intro; auto.
        * do 2 rewrite lb_pointwise_cons; f_equal; auto.
    Qed.

    Variable (Hf1 : forall x a b, leb a b -> leb (f x a) (f x b)) 
             (Hf2 : f ⟘ ⟘ = ⟘).

    Let lbpw_mono_1 l m :  lb_pointwise l nil ⪯   lb_pointwise l m.
    Proof.
(* Goal: @eq (list bool) (lb_pointwise orb x (@nil bool)) x *)
      rewrite lb_pointwise_left.
(* Goal: lb_mask (@map bool bool (fun x : bool => f x false) l) (lb_pointwise l m) *)
      revert m; induction l as [ | x l IHl ]; intros m.
      + simpl; constructor.
      + destruct m as [ | y m ]; simpl.
        * apply lb_mask_refl.
        * apply lb_mask_leb; auto.
    Qed.

    Let lbpw_mono_f_0 g l m : g ⟘ = ⟘ -> leb (g ⟘) (g ⟙) -> l ⪯ m -> map g l ⪯  map g m.
    Proof.
(* Goal: forall (_ : lb_mask l m) (_ : lb_mask a b), lb_mask (lb_join l a) (lb_join m b) *)
      intros H1 H2.
(* Goal: forall _ : lb_mask l m, lb_mask (@map bool bool g l) (@map bool bool g m) *)
      assert (Hg : forall x y, x ⪦ y -> g x ⪦ g y).
(* Goal: forall (x y : bool) (_ : leb x y), leb (g x) (g y) *)
(* Goal: forall _ : lb_mask l m, lb_mask (@map bool bool g l) (@map bool bool g m) *)
      { intros [] []; simpl; auto; discriminate. }
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
      induction 1; simpl; try rewrite H1; constructor; auto.
    Qed.

    Let lbpw_mono_2 l m : m ⪯ nil -> lb_pointwise l m ⪯   lb_pointwise l nil.
    Proof.
(* Goal: forall _ : lb_mask m (@nil bool), lb_mask (lb_pointwise l m) (lb_pointwise l (@nil bool)) *)
      revert m; induction l as [ | x l IHl ]; intros [ | y m ] H.
      + constructor.
      + rewrite lb_pointwise_right.
(* Goal: lb_mask (@map bool bool (f false) (@cons bool y m)) (lb_pointwise (@nil bool) (@nil bool)) *)
        apply lbpw_mono_f_0 with (g := f ⟘) in H; auto.
      + apply lb_mask_refl.
      + rewrite lb_pointwise_cons, lb_pointwise_left.
(* Goal: lb_mask (@cons bool (f x y) (lb_pointwise l m)) (@map bool bool (fun x : bool => f x false) (@cons bool x l)) *)
        apply lb_mask_inv_left in H.
(* Goal: lb_mask (@cons bool (f x y) (lb_pointwise l m)) (@map bool bool (fun x : bool => f x false) (@cons bool x l)) *)
        destruct H as (E & H); subst y.
(* Goal: lb_mask (@cons bool (f x false) (lb_pointwise l m)) (@map bool bool (fun x : bool => f x false) (@cons bool x l)) *)
        simpl.
(* Goal: lb_mask (@cons bool (f x false) (lb_pointwise l m)) (@cons bool (f x false) (@map bool bool (fun x : bool => f x false) l)) *)
        apply lb_mask_leb.
(* Goal: leb (f x false) (f x false) *)
(* Goal: lb_mask (lb_pointwise l m) (@map bool bool (fun x : bool => f x false) l) *)
        1: destruct (f x ⟘); simpl; auto.
(* Goal: lb_mask (lb_pointwise l m) (@map bool bool (fun x : bool => f x false) l) *)
        apply lb_mask_trans with (1 := IHl _ H).
(* Goal: @eq (list bool) (lb_pointwise orb x (@nil bool)) x *)
        rewrite lb_pointwise_left.
(* Goal: lb_mask (@map bool bool (fun x : bool => f x false) l) (@map bool bool (fun x : bool => f x false) l) *)
        apply lb_mask_refl.
    Qed.

    Fact lb_pointwise_mono_left l m k : l ⪯  m -> lb_pointwise k l ⪯   lb_pointwise k m.
    Proof.
(* Goal: forall _ : lb_mask l m, lb_mask (lb_pointwise k l) (lb_pointwise k m) *)
      intros H; revert m H k.
(* Goal: forall (m : list bool) (_ : lb_mask l m) (k : list bool), lb_mask (lb_pointwise k l) (lb_pointwise k m) *)
      induction l as [ | x l IHl ]; intros m H k; auto.
(* Goal: lb_mask (lb_pointwise k (@cons bool x l)) (lb_pointwise k m) *)
      destruct m as [ | y m ].
      * apply lbpw_mono_2; auto.
      * destruct k as [ | u k ].
        - apply lbpw_mono_f_0; auto.
        - do 2 rewrite lb_pointwise_cons.
(* Goal: lb_mask (@cons bool (f u x) (lb_pointwise k l)) (@cons bool (f u y) (lb_pointwise k m)) *)
          apply lb_mask_inv_cons in H; destruct H.
(* Goal: lb_mask (@cons bool (andb x y) (lb_meet a b)) (@cons bool x a) *)
          apply lb_mask_leb; auto.
    Qed.
  
  End lb_pointwise.

  Definition lb_meet := (lb_pointwise andb).
  Definition lb_join := (lb_pointwise orb).

  Local Infix "↓" := lb_meet.
  Local Infix "↑" := lb_join.

  Fact lb_meet_left x : x↓nil ≂ nil.
  Proof.
(* Goal: lb_mask_equiv (lb_meet x (@nil bool)) (@nil bool) *)
    unfold lb_meet.
(* Goal: lb_mask_equiv (lb_pointwise andb x (@nil bool)) (@nil bool) *)
    split; try (constructor; fail).
(* Goal: @eq (list bool) (lb_pointwise orb x (@nil bool)) x *)
    rewrite lb_pointwise_left.
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
    induction x as [ | [] x ]; simpl; constructor; auto.
  Qed.

  Fact lb_meet_comm l m : l↓m = m↓l.
  Proof.
(* Goal: @eq (list bool) (lb_join l m) (lb_join m l) *)
    apply lb_pointwise_sym.
(* Goal: forall x y : bool, @eq bool (orb x y) (orb y x) *)
    destruct x; destruct y; auto.
  Qed.

  Fact lb_meet_right x : nil↓x ≂ nil.
  Proof.
(* Goal: lb_mask_equiv (lb_meet (@nil bool) x) (@nil bool) *)
    rewrite lb_meet_comm; apply lb_meet_left.
  Qed.

  Fact lb_meet_cons x y l m : (x::l) ↓ (y::m) = x && y :: l↓m.
  Proof. auto. Qed.

  Fact lb_meet_mono l m a b : l ⪯ m -> a ⪯ b -> l↓a ⪯  m↓b.
  Proof.
(* Goal: forall (_ : lb_mask l m) (_ : lb_mask a b), lb_mask (lb_join l a) (lb_join m b) *)
    intros H1 H2.
(* Goal: lb_mask (lb_meet l a) (lb_meet m b) *)
    apply lb_mask_trans with (l↓b).
    + apply lb_pointwise_mono_left;auto.
(* Goal: forall (x a b : bool) (_ : leb a b), leb (orb x a) (orb x b) *)
      intros [] [] []; simpl; auto; discriminate.
    + do 2 rewrite (lb_meet_comm _ b).
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      apply lb_pointwise_mono_left;auto.
(* Goal: forall (x a b : bool) (_ : leb a b), leb (orb x a) (orb x b) *)
      intros [] [] []; simpl; auto; discriminate.
  Qed.

  Add Parametric Morphism: (lb_meet) with signature (lbeq) ==> (lbeq) ==> (lbeq) as lb_meet_eq.
  Proof. intros ? ? [] ? ? []; split; apply lb_meet_mono; auto. Qed.

  Fact lb_meet_length_le n l m : length l <= n -> length m <= n -> length (l↓m) <= n.
  Proof. apply lb_pointwise_length. Qed.

  Fact lb_meet_length a b : length a = length b -> length (a↓b) = length a.
  Proof.
    revert b; induction a as [ | x a IHa ]; intros [ | y b ]; try discriminate; auto;
(* Goal: forall _ : lb_mask a b, @sig (list bool) (fun c : list bool => and (lb_ortho a c) (lb_mask_equiv b (lb_join a c))) *)
      intros H.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    rewrite lb_meet_cons; simpl; f_equal; auto.
  Qed.

  Fact lb_meet_app l m a b : length l = length m -> (l++a)↓(m++b) = l↓m++a↓b.   
  Proof.
(* Goal: forall _ : @eq nat (@length bool l) (@length bool m), @eq (list bool) (lb_meet (@app bool l a) (@app bool m b)) (@app bool (lb_meet l m) (lb_meet a b)) *)
    revert m; induction l as [ | x l IHl ]; intros [ | y m ]; try discriminate; intros H.
    + simpl; auto.
    + simpl app.
(* Goal: @eq (list bool) (lb_meet (@cons bool x (@app bool l a)) (@cons bool y (@app bool m b))) (@cons bool (andb x y) (@app bool (lb_meet l m) (lb_meet a b))) *)
      rewrite lb_meet_cons; f_equal.
(* Goal: @eq (list bool) (lb_meet (@app bool l a) (@app bool m b)) (@app bool (lb_meet l m) (lb_meet a b)) *)
      apply IHl.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      simpl in H; inversion H; auto.
  Qed.

  Fact lb_join_left x : x↑nil = x.
  Proof.
(* Goal: @eq (list bool) (lb_join x (@nil bool)) x *)
    unfold lb_join.
(* Goal: @eq (list bool) (lb_pointwise orb x (@nil bool)) x *)
    rewrite lb_pointwise_left.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    induction x as [ | [] ]; simpl; f_equal; auto.
  Qed.

  Fact lb_join_comm l m : l↑m = m↑l.
  Proof.
(* Goal: @eq (list bool) (lb_join l m) (lb_join m l) *)
    apply lb_pointwise_sym.
(* Goal: forall x y : bool, @eq bool (orb x y) (orb y x) *)
    destruct x; destruct y; auto.
  Qed.

  Fact lb_join_right x : nil↑x = x.
  Proof.
(* Goal: @eq (list bool) (lb_join (@nil bool) x) x *)
    rewrite lb_join_comm; apply lb_join_left.
  Qed.
 
  Fact lb_join_cons x y l m : (x::l) ↑ (y::m) = x || y :: l↑m.
  Proof. auto. Qed.

  Fact lb_join_length_le n l m : length l <= n -> length m <= n -> length (l↑m) <= n.
  Proof. apply lb_pointwise_length. Qed.

  Fact lb_join_mono l m a b : l ⪯ m -> a ⪯ b -> l↑a ⪯  m↑b.
  Proof.
(* Goal: forall (_ : lb_mask l m) (_ : lb_mask a b), lb_mask (lb_join l a) (lb_join m b) *)
    intros H1 H2.
(* Goal: lb_mask (lb_join l a) (lb_join m b) *)
    apply lb_mask_trans with (l↑b).
    + apply lb_pointwise_mono_left;auto.
(* Goal: forall (x a b : bool) (_ : leb a b), leb (orb x a) (orb x b) *)
      intros [] [] []; simpl; auto; discriminate.
    + do 2 rewrite (lb_join_comm _ b).
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      apply lb_pointwise_mono_left;auto.
(* Goal: forall (x a b : bool) (_ : leb a b), leb (orb x a) (orb x b) *)
      intros [] [] []; simpl; auto; discriminate.
  Qed.

  Add Parametric Morphism: (lb_join) with signature (lbeq) ==> (lbeq) ==> (lbeq) as lb_join_eq.
  Proof. intros ? ? [] ? ? []; split; apply lb_join_mono; auto. Qed.

  Fact lb_ortho_meet_nil x y : x ⟂ y <-> x↓y ≂ nil.
  Proof.
(* Goal: iff (lb_mask a b) (lb_mask_equiv (lb_meet a b) a) *)
    split.
    + intros H; split; try constructor; revert H.
(* Goal: forall _ : lb_ortho x y, lb_mask (lb_meet x y) (@nil bool) *)
      induction 1 as [ m | l | x y l m ].
(* Goal: lb_mask (@nil bool) (lb_meet (@nil bool) l) *)
      - rewrite lb_meet_right; constructor.
(* Goal: lb_mask (@nil bool) (lb_meet (@nil bool) l) *)
      - rewrite lb_meet_left; constructor.
      - rewrite lb_meet_cons.
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
        simpl; destruct H; [ destruct y | destruct x ]; try discriminate; subst; simpl; constructor; auto.
    + intros [ H1 _ ]; revert H1.
(* Goal: forall _ : lb_mask (lb_meet x y) (@nil bool), lb_ortho x y *)
      revert y; induction x as [ | x l IHl ]; intros [ | y m ]; simpl; intros H; try (constructor; fail).
      destruct x; destruct y; simpl in H |- *; try (inversion H; fail);
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
        apply lb_mask_inv_nil in H; constructor; auto.
  Qed.

  Hint Resolve lb_mask_equiv_refl.

  Fact lb_join_inc_left a b : a ⪯  a↑b.
  Proof.
(* Goal: @sig (list bool) (fun c : list bool => and (lb_ortho b c) (lb_mask_equiv (lb_join a b) (lb_join c b))) *)
    revert b; induction a as [ | x a IHa ]; intros b.
    + constructor.
    + destruct b as [ | y b ].
      * rewrite lb_join_left; auto.
      * rewrite lb_join_cons.
(* Goal: lb_mask (@cons bool (andb x y) (lb_meet a b)) (@cons bool x a) *)
        apply lb_mask_leb; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
        destruct x; destruct y; simpl; auto.
  Qed.

  Fact lb_meet_dec_left a b : a↓b ⪯  a.
  Proof.
(* Goal: @sig (list bool) (fun c : list bool => and (lb_ortho b c) (lb_mask_equiv (lb_join a b) (lb_join c b))) *)
    revert b; induction a as [ | x a IHa ]; intros b.
    + rewrite lb_meet_right; constructor.
    + destruct b as [ | y b ].
      * rewrite lb_meet_left; constructor. 
      * rewrite lb_meet_cons.
(* Goal: lb_mask (@cons bool (andb x y) (lb_meet a b)) (@cons bool x a) *)
        apply lb_mask_leb; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
        destruct x; destruct y; simpl; auto.
  Qed.

  Fact lb_join_inc_right a b : b ⪯  a↑b.
  Proof. rewrite lb_join_comm; apply lb_join_inc_left. Qed.

  Fact lb_meet_dec_right a b : a↓b ⪯  b.
  Proof. rewrite lb_meet_comm; apply lb_meet_dec_left. Qed.
  
  Hint Resolve lb_join_inc_left lb_join_inc_right lb_meet_dec_left lb_meet_dec_right.

  Fact lb_mask_join a b : a ⪯  b <-> a↑b ≂ b.
  Proof.
(* Goal: iff (lb_mask a b) (lb_mask_equiv (lb_meet a b) a) *)
    split.
    + intros H; split.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      2: rewrite lb_join_comm; auto.
(* Goal: lb_mask a (lb_meet a b) *)
      induction H as [ | | x y ? ? H ].
      * rewrite lb_join_right; auto.
      * rewrite lb_join_left; constructor; auto.
      * rewrite lb_join_cons; constructor; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
        revert x y H; intros [] []; simpl; auto.
    + intros (H1 & _).
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      apply lb_mask_trans with (2 := H1); auto.
  Qed.

  Fact lb_mask_meet a b : a ⪯  b <-> a↓b ≂ a.
  Proof.
(* Goal: iff (lb_mask a b) (lb_mask_equiv (lb_meet a b) a) *)
    split.
    + intros H; split; auto.
(* Goal: lb_mask a (lb_meet a b) *)
      induction H as [ | | x y ? ? H ].
      * constructor.
      * rewrite lb_meet_left; constructor; auto.
      * rewrite lb_meet_cons; constructor; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
        revert x y H; intros [] []; simpl; auto.
    + intros (H1 & H2).
(* Goal: lb_mask a b *)
      apply lb_mask_trans with (1 := H2).
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      rewrite lb_meet_comm; auto.
  Qed.

  Fact lb_meet_idem a : a↓a = a.
  Proof.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    induction a as [ | x a ]; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    rewrite lb_meet_cons; f_equal; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    destruct x; simpl; auto.
  Qed.

  Fact lb_join_idem a : a↑a = a.
  Proof.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    induction a as [ | x a ]; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    rewrite lb_join_cons; f_equal; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    destruct x; simpl; auto.
  Qed.

  Tactic Notation "rew" "lb"  :=
       repeat (  rewrite lb_meet_left || rewrite lb_meet_right
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
              || rewrite lb_join_left || rewrite lb_join_right); auto.

  Fact lb_join_meet_distr a b c : a↑(b↓c) ≂ (a↑b)↓(a↑c).
  Proof.
(* Goal: lb_mask_equiv (lb_join a (lb_join b c)) (lb_join (lb_join a b) c) *)
    revert b c; induction a as [ | x a IHa ]; intros b c.
    + rew lb.
    + destruct b as [ | y b ].
      * rew lb.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
        rewrite (proj1 (lb_mask_meet _ _)); auto.
      * destruct c as [ | z c ].
        - rew lb.
(* Goal: lb_mask_equiv (@cons bool x a) (lb_meet (lb_join (@cons bool x a) (@cons bool y b)) (@cons bool x a)) *)
          rewrite lb_meet_comm. 
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          rewrite (proj1 (lb_mask_meet _ _)); auto.
        - repeat rewrite lb_meet_cons.
(* Goal: lb_mask (@cons bool x a) (lb_join (@cons bool x a) (@cons bool y b)) *)
          repeat rewrite lb_join_cons.
(* Goal: lb_mask (lb_meet (@cons bool x a) (@cons bool y b)) (@cons bool x a) *)
          repeat rewrite lb_meet_cons.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          apply lb_mask_equiv_cons; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          destruct x; destruct y; destruct z; simpl; auto.
  Qed.

  Fact lb_meet_join_distr a b c : a↓(b↑c) ≂ (a↓b)↑(a↓c).
  Proof.
(* Goal: lb_mask_equiv (lb_join a (lb_join b c)) (lb_join (lb_join a b) c) *)
    revert b c; induction a as [ | x a IHa ]; intros b c.
    + rew lb.
    + destruct b as [ | y b ].
      * rew lb.
      * destruct c as [ | z c ].
        - rew lb.
        - repeat rewrite lb_meet_cons.
(* Goal: lb_mask (@cons bool x a) (lb_join (@cons bool x a) (@cons bool y b)) *)
          repeat rewrite lb_join_cons.
(* Goal: lb_mask (lb_meet (@cons bool x a) (@cons bool y b)) (@cons bool x a) *)
          repeat rewrite lb_meet_cons.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          apply lb_mask_equiv_cons; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          destruct x; destruct y; destruct z; simpl; auto.
  Qed.

  Fact lb_meet_assoc a b c : a↓(b↓c) ≂ a↓b↓c.
  Proof.
(* Goal: lb_mask_equiv (lb_join a (lb_join b c)) (lb_join (lb_join a b) c) *)
    revert b c; induction a as [ | x a IHa ]; intros b c.
    + rew lb.
    + destruct b as [ | y b ].
      * rew lb.
      * destruct c as [ | z c ].
        - rew lb.
        - repeat rewrite lb_meet_cons.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          apply lb_mask_equiv_cons; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          destruct x; destruct y; destruct z; simpl; auto.
  Qed.

  Fact lb_join_assoc a b c : a↑(b↑c) ≂ a↑b↑c.
  Proof.
(* Goal: lb_mask_equiv (lb_join a (lb_join b c)) (lb_join (lb_join a b) c) *)
    revert b c; induction a as [ | x a IHa ]; intros b c.
    + rew lb.
    + destruct b as [ | y b ].
      * rew lb.
      * destruct c as [ | z c ].
        - rew lb.
        - repeat rewrite lb_join_cons.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          apply lb_mask_equiv_cons; auto.
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
          destruct x; destruct y; destruct z; simpl; auto.
  Qed.

  Hint Resolve lb_meet_mono lb_join_mono.
  
  Fact lb_join_spec a b c : a ⪯  c -> b ⪯  c -> a↑b ⪯  c.
  Proof. intros; rewrite <- (lb_join_idem c); auto. Qed.

  Fact lb_meet_spec a b c : c ⪯  a -> c ⪯  b -> c ⪯  a↓b.
  Proof. intros; rewrite <- (lb_meet_idem c); auto. Qed.

  Fact lb_meet_join_idem a b : a↓(a↑b) ≂ a.
  Proof. rewrite <- lb_mask_meet; auto. Qed.

  Fact lb_join_meet_idem a b : a↑(a↓b) ≂ a.
  Proof. rewrite lb_join_comm, <- lb_mask_join; auto. Qed.

  Fact lb_join_nil_eq a b : a↑b ≂ nil -> a ≂ nil /\ b ≂ nil.
  Proof.
(* Goal: iff (lb_mask a b) (lb_mask_equiv (lb_meet a b) a) *)
    intros H; split.
    rewrite <- (lb_meet_left a), <- H, lb_meet_join_idem; auto.
    rewrite <- (lb_meet_left b), <- H, lb_join_comm, lb_meet_join_idem; auto.
  Qed.

  Fact lb_ortho_join a x y : a ⟂ x↑y <-> a ⟂ x /\ a ⟂ y.
  Proof.
(* Goal: iff (lb_mask a b) (lb_mask_equiv (lb_meet a b) a) *)
    do 3 rewrite lb_ortho_meet_nil; split.
    + intros H; apply lb_join_nil_eq.
      rewrite <- lb_meet_join_distr, H; auto.
    + intros (H1 & H2).
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
      rewrite lb_meet_join_distr, H1, H2; auto.
  Qed.

  Fact lb_ortho_mask_nil a x : a ⟂ x -> x ⪯  a -> x ≂ nil.
  Proof. 
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
    induction 1 as [ | | x y l m H1 H2 IH2 ]; auto.
    + split; auto.
    + intros H.
(* Goal: lb_mask_equiv (@cons bool y m) (@nil bool) *)
      apply lb_mask_inv_cons in H; destruct H as (H3 & H4).
(* Goal: forall _ : lb_mask l (@nil bool), lb_mask_equiv l (@nil bool) *)
      rewrite IH2; auto; split; auto.
(* Goal: lb_mask (@cons bool y (@nil bool)) (@nil bool) *)
      revert x y H1 H3.
(* Goal: lb_ortho (@cons bool x l) (@cons bool v z) *)
      intros [] []; simpl; intros [] ?; try discriminate; constructor; auto.
  Qed.

  (* c = a - b *)

  Section lb_complement.

    Let bin_comp a b :=
      match a, b with
        | ⟘, ⟘  => ⟘ 
        | ⟘, ⟙  => ⟘
        | ⟙, ⟘  => ⟙
        | ⟙, ⟙  => ⟘ 
    end.

(* Goal: forall (x y : bool) (_ : leb x y), leb (g x) (g y) *)
(* Goal: forall _ : lb_mask l m, lb_mask (@map bool bool g l) (@map bool bool g m) *)
    Definition lb_complement a b : { c | b ⟂ c /\ a↑b ≂ c↑b }.
    Proof.
(* Goal: @sig (list bool) (fun c : list bool => and (lb_ortho b c) (lb_mask_equiv (lb_join a b) (lb_join c b))) *)
       revert b; induction a as [ | x a IHa ]; intros b.
       + exists nil; split; auto.
       + destruct b as [ | y b ].
(* Goal: forall _ : lb_mask l (@nil bool), lb_mask_equiv l (@nil bool) *)
         - exists (x :: a); split; auto.
         - destruct (IHa b) as (c & H1 & H2).
(* Goal: @sig (list bool) (fun c : list bool => and (lb_ortho (@cons bool y b) c) (lb_mask_equiv (lb_join (@cons bool x a) (@cons bool y b)) (lb_join c (@cons bool y b)))) *)
           exists (bin_comp x y::c).
           revert x y; intros [] []; simpl; split; auto; 
(* Goal: @eq (list bool) (lb_join (@cons bool x l) (@cons bool y m)) (@cons bool (orb x y) (lb_join l m)) *)
             rewrite H2; simpl; auto.
    Qed.

  End lb_complement.

(* Goal: forall (x y : bool) (_ : leb x y), leb (g x) (g y) *)
(* Goal: forall _ : lb_mask l m, lb_mask (@map bool bool g l) (@map bool bool g m) *)
  Definition lb_minus a b : a ⪯ b -> { c | a ⟂ c /\ b ≂ a↑c }.
  Proof.
(* Goal: forall _ : lb_mask a b, @sig (list bool) (fun c : list bool => and (lb_ortho a c) (lb_mask_equiv b (lb_join a c))) *)
    intros H.
(* Goal: @sig (list bool) (fun c : list bool => and (lb_ortho a c) (lb_mask_equiv b (lb_join a c))) *)
    destruct (lb_complement b a) as (c & H1 & H2).
(* Goal: forall _ : lb_mask l (@nil bool), lb_mask_equiv l (@nil bool) *)
    exists c; split; auto.
(* Goal: lb_mask_equiv b (lb_join a c) *)
    rewrite lb_mask_join in H.
    rewrite <- H, (lb_join_comm a), (lb_join_comm a); auto.
  Qed.

(* End lb.

Hint Resolve leb_refl leb_trans leb_strict.
Hint Resolve lb_mask_refl lb_mask_trans.
Hint Resolve in_lb_mask_0 lb_mask_refl lb_mask_equiv_refl.
Hint Constructors lb_mask lb_ortho.
Hint Resolve lb_mask_equiv_refl.
Hint Resolve lb_join_inc lb_meet_dec_left lb_meet_dec_right.
*)
