text:
Require Export Coq.Lists.List.
Require Export Coq.ZArith.ZArith.
Require Export compcert.lib.Coqlib.
Require Export compcert.lib.Integers.
Require Export compcert.lib.Floats.
Require Export compcert.common.Values.
Require Export VST.msl.eq_dec.
Require Export VST.msl.Coqlib2.
Require Export VST.floyd.coqlib3.
Require Export VST.zlist.sublist.
Require Export Lia.
Require Export VST.zlist.list_solver.

Definition Vubyte (c: Byte.int) : val :=
  Vint (Int.repr (Byte.unsigned c)).
Definition Vbyte (c: Byte.int) : val :=
  Vint (Int.repr (Byte.signed c)).
Ltac fold_Vbyte :=
 repeat match goal with |- context [Vint (Int.repr (Byte.signed ?c))] =>
      fold (Vbyte c)
end.
Ltac  customizable_list_solve_preprocess ::= fold_Vbyte.
#[export] Instance Inhabitant_val : Inhabitant val := Vundef.
#[export] Instance Inhabitant_int: Inhabitant int := Int.zero.
#[export] Instance Inhabitant_byte: Inhabitant byte := Byte.zero.
#[export] Instance Inhabitant_int64: Inhabitant Int64.int := Int64.zero.
#[export] Instance Inhabitant_ptrofs: Inhabitant Ptrofs.int := Ptrofs.zero.
#[export] Instance Inhabitant_float : Inhabitant float := Float.zero.
#[export] Instance Inhabitant_float32 : Inhabitant float32 := Float32.zero.

#[export] Hint Rewrite (@Znth_map _ Inhabitant_float) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_float32) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_ptrofs) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_int64) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_byte) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_int) using Zlength_solve : Znth.
#[export] Hint Rewrite (@Znth_map _ Inhabitant_val) using Zlength_solve : Znth.

Create HintDb entailer_rewrite discriminated.

Require Import VST.veric.val_lemmas.

Lemma Vint_injective i j (H: Vint i = Vint j): i=j.
Proof. inv H; trivial. Qed.

Lemma map_Vint_injective: forall l m, map Vint l = map Vint m -> l=m.
Proof. induction l; intros.
+ destruct m; inv H; trivial.
+ destruct m; inv H. f_equal; eauto.
Qed.

Lemma cons_inv {A} (a a':A) l l': a::l = a'::l' -> a=a' /\ l=l'.
Proof. intros. inv H; eauto. Qed.

#[export] Hint Rewrite
   (@Znth_map val _) (@Znth_map int _) (@Znth_map byte _)
   (@Znth_map int64 _) (@Znth_map ptrofs _) (@Znth_map float _)
   (@Znth_map float32 _)
    using (auto; rewrite ?Zlength_map in *; lia) : sublist entailer_rewrite.

Lemma is_long_dec v: {is_long v} + {~ is_long v}.
Proof. destruct v; simpl; try solve [right; intros N; trivial]; left; trivial. Defined.

Lemma is_single_dec v: {is_single v} + {~ is_single v}.
Proof. destruct v; simpl; try solve [right; intros N; trivial]; left; trivial. Defined.

Lemma is_float_dec v: {is_float v} + {~ is_float v}.
Proof. destruct v; simpl; try solve [right; intros N; trivial]; left; trivial. Defined.

Lemma is_pointer_or_integer_dec v: {is_pointer_or_integer v} + {~ is_pointer_or_integer v}.
Proof.
unfold is_pointer_or_integer.
destruct Archi.ptr64 eqn:Hp;
destruct v; simpl; try solve [right; intros N; trivial]; left; trivial.
Defined.

Lemma is_pointer_or_null_dec v: {is_pointer_or_null v} + {~ is_pointer_or_null v}.
Proof. destruct v; simpl; try solve [right; intros N; trivial]; try solve [left; trivial].
 try apply Int.eq_dec;  (* this line works for CompCert 3.3 *)
 destruct Archi.ptr64; auto; apply Int64.eq_dec.  (* this line needed for newer CompCert *)
Defined.

Lemma isptr_dec v: {isptr v} + {~ isptr v}.
Proof. destruct v; simpl; try solve [right; intros N; trivial]; left; trivial. Defined.

Lemma isptr_offset_val':
 forall i p, isptr p -> isptr (offset_val i p).
Proof. intros. destruct p; try contradiction; apply Coq.Init.Logic.I. Qed.
#[export] Hint Extern 1 (isptr (offset_val _ _)) => apply isptr_offset_val' : core.
#[export] Hint Resolve isptr_offset_val': norm.

Lemma offset_val_force_ptr:
  offset_val 0 = force_ptr.
Proof. extensionality v. destruct v; try reflexivity.
simpl. rewrite Ptrofs.add_zero; auto.
Qed.
#[export] Hint Rewrite <- offset_val_force_ptr : norm.

Lemma offset_offset_val:
  forall v i j, offset_val j (offset_val i v) = offset_val (i + j) v.
Proof. intros; unfold offset_val.
 destruct v; auto.
 f_equal. rewrite Ptrofs.add_assoc. f_equal. apply ptrofs_add_repr.
Qed.
#[export] Hint Rewrite offset_offset_val: norm.

#[export] Hint Rewrite add_repr add64_repr ptrofs_add_repr : norm.
#[export] Hint Rewrite mul_repr mul64_repr ptrofs_mul_repr : norm.
#[export] Hint Rewrite sub_repr sub64_repr ptrofs_sub_repr : norm.
#[export] Hint Rewrite and_repr and64_repr : norm.
#[export] Hint Rewrite or_repr or64_repr : norm.
#[export] Hint Rewrite neg_repr neg64_repr : norm.

Lemma ltu_repr: forall i j,
 (0 <= i <= Int.max_unsigned ->
  0 <= j <= Int.max_unsigned ->
  Int.ltu (Int.repr i) (Int.repr j) = true -> i<j)%Z.
Proof.
intros. unfold Int.ltu in H1. if_tac in H1; inv H1.
repeat rewrite Int.unsigned_repr in H2 by assumption.
auto.
Qed.

Lemma ltu_repr64: forall i j,
 (0 <= i <= Int64.max_unsigned ->
  0 <= j <= Int64.max_unsigned ->
  Int64.ltu (Int64.repr i) (Int64.repr j) = true -> i<j)%Z.
Proof.
intros. unfold Int64.ltu in H1. if_tac in H1; inv H1.
repeat rewrite Int64.unsigned_repr in H2 by assumption.
auto.
Qed.

Lemma ltu_repr_false: forall i j,
 (0 <= i <= Int.max_unsigned ->
  0 <= j <= Int.max_unsigned ->
  Int.ltu (Int.repr i) (Int.repr j) = false -> i>=j)%Z.
Proof.
intros. unfold Int.ltu in H1. if_tac in H1; inv H1.
repeat rewrite Int.unsigned_repr in H2 by assumption.
auto.
Qed.

Lemma ltu_repr_false64: forall i j,
 (0 <= i <= Int64.max_unsigned ->
  0 <= j <= Int64.max_unsigned ->
  Int64.ltu (Int64.repr i) (Int64.repr j) = false -> i>=j)%Z.
Proof.
intros. unfold Int64.ltu in H1. if_tac in H1; inv H1.
repeat rewrite Int64.unsigned_repr in H2 by assumption.
auto.
Qed.

Lemma ltu_inv:
 forall x y, Int.ltu x y = true -> Int.unsigned x < Int.unsigned y.
Proof.
intros.
apply Int.ltu_inv in H; destruct H; auto.
Qed.

Lemma ltu_inv64:
 forall x y, Int64.ltu x y = true -> Int64.unsigned x < Int64.unsigned y.
Proof.
intros.
apply Int64.ltu_inv in H; destruct H; auto.
Qed.

Lemma ltu_false_inv:
 forall x y, Int.ltu x y = false -> Int.unsigned x >= Int.unsigned y.
Proof.
intros.
unfold Int.ltu in H. if_tac in H; inv H; auto.
Qed.

Lemma ltu_false_inv64:
 forall x y, Int64.ltu x y = false -> Int64.unsigned x >= Int64.unsigned y.
Proof.
intros.
unfold Int64.ltu in H. if_tac in H; inv H; auto.
Qed.

Definition repable_signed (z: Z) :=
  Int.min_signed <= z <= Int.max_signed.

Lemma lt_repr:
     forall i j : Z,
       repable_signed i ->
       repable_signed j ->
       Int.lt (Int.repr i) (Int.repr j) = true -> (i < j)%Z.
Proof.
intros.
unfold Int.lt in H1. if_tac in H1; inv H1.
rewrite !Int.signed_repr in H2 by auto.
auto.
Qed.

Lemma int_add_assoc1:
  forall z i j, Int.add (Int.add z (Int.repr i)) (Int.repr j) = Int.add z (Int.repr (i+j)).
Proof.
intros.
rewrite Int.add_assoc. f_equal. apply add_repr.
Qed.
#[export] Hint Rewrite int_add_assoc1 : norm.

Lemma ptrofs_add_assoc1:
  forall z i j, Ptrofs.add (Ptrofs.add z (Ptrofs.repr i)) (Ptrofs.repr j) = Ptrofs.add z (Ptrofs.repr (i+j)).
Proof.
intros.
rewrite Ptrofs.add_assoc. f_equal. apply ptrofs_add_repr.
Qed.
#[export] Hint Rewrite ptrofs_add_assoc1 : norm.

Lemma divide_add_align: forall a b c, Z.divide b a -> a + (align c b) = align (a + c) b.
Proof.
  intros.
  pose proof zeq b 0.
  destruct H0; unfold Z.divide in H; unfold align.
  + destruct H. subst.
    repeat rewrite Zdiv_0_r.
    simpl.
    lia.
  + destruct H.
    subst.
    replace (x * b + c + b - 1) with (x * b + (c + b - 1)) by lia.
    rewrite Z_div_plus_full_l.
    rewrite Z.mul_add_distr_r.
    reflexivity.
    lia.
Qed.

Lemma force_val_e:
 forall v, force_val (Some v) = v.
Proof. reflexivity. Qed.
#[export] Hint Rewrite force_val_e: norm.

Definition ptr_eq (v1 v2: val) : Prop :=
      match v1,v2 with
      | Vint n1, Vint n2 =>  Archi.ptr64 = false /\ Int.cmpu Ceq n1 n2 = true  /\ Int.cmpu Ceq n1 (Int.repr 0) = true
      | Vlong n1, Vlong n2 =>  Archi.ptr64 = true /\ Int64.cmpu Ceq n1 n2 = true  /\ Int64.cmpu Ceq n1 (Int64.repr 0) = true
      | Vptr b1 ofs1,  Vptr b2 ofs2  =>
            b1=b2 /\ Ptrofs.cmpu Ceq ofs1 ofs2 = true
      | _,_ => False
      end.

Definition ptr_neq (v1 v2: val) := ~ ptr_eq v1 v2.

Lemma ptr_eq_e: forall v1 v2, ptr_eq v1 v2 -> v1=v2.
Proof.
intros. destruct v1; destruct v2; simpl in H; try contradiction.
*
pose proof (Int.eq_spec i i0). destruct H as [Hp [? ?]].
rewrite H in H0. subst; auto.
*
pose proof (Int64.eq_spec i i0). destruct H as [Hp [? ?]].
rewrite H in H0. subst; auto.
*
destruct H; subst.
f_equal.
pose proof (Ptrofs.eq_spec i i0). rewrite H0 in H; auto.
Qed.

Lemma ptr_eq_True':
   forall p, isptr p -> ptr_eq p p = True.
Proof. intros.
 apply prop_ext; intuition. destruct p; inv H; simpl; auto.
 rewrite Ptrofs.eq_true. auto.
Qed.
(* #[export] Hint Rewrite ptr_eq_True' using solve[auto] : norm. *)

Lemma ptr_eq_True:
   forall p, is_pointer_or_null p -> ptr_eq p p = True.
Proof. intros.
 apply prop_ext; intuition. destruct p; inv H; simpl; auto.
 rewrite Ptrofs.eq_true. auto.
Qed.
#[export] Hint Rewrite ptr_eq_True using solve[auto] : norm.

Lemma ptr_eq_is_pointer_or_null: forall x y, ptr_eq x y -> is_pointer_or_null x.
Proof.
  intros.
  unfold ptr_eq, is_pointer_or_null in *.
  destruct x; destruct y; try tauto;
  destruct H as [Hp [_ ?]]; rewrite Hp.
  unfold Int.cmpu in H.
  pose proof (Int.eq_spec i (Int.repr 0)). rewrite H in H0. auto.
  unfold Int64.cmpu in H.
  pose proof (Int64.eq_spec i (Int64.repr 0)). rewrite H in H0. auto.
Qed.

Lemma ptr_eq_sym: forall x y, ptr_eq x y -> ptr_eq y x.
Proof.
   intros.
   pose proof ptr_eq_is_pointer_or_null _ _ H.
   apply ptr_eq_e in H.
   rewrite H in *.
   rewrite ptr_eq_True; tauto.
Qed.

Lemma ptr_eq_trans: forall x y z, ptr_eq x y -> ptr_eq y z -> ptr_eq x z.
Proof.
   intros.
   pose proof ptr_eq_is_pointer_or_null _ _ H.
   apply ptr_eq_e in H.
   apply ptr_eq_e in H0.
   subst.
   rewrite ptr_eq_True; tauto.
Qed.

Lemma isptr_offset_val_zero:
  forall v, isptr v -> offset_val 0 v = v.
Proof. intros. destruct v; inv H; subst; simpl.  rewrite Ptrofs.add_zero; reflexivity.
Qed.

#[export] Hint Rewrite isptr_offset_val_zero using solve [auto] : norm.

Lemma isptr_offset_val:
 forall i p, isptr (offset_val i p) = isptr p.
Proof.
intros.
unfold isptr.
destruct p; simpl; auto.
Qed.
#[export] Hint Rewrite isptr_offset_val : norm.

Lemma isptr_force_ptr: forall v, isptr v -> force_ptr v = v.
Proof. intros. destruct v; inv H; auto. Qed.
#[export] Hint Rewrite isptr_force_ptr using solve [auto] : norm.

Lemma isptr_force_ptr' : forall p, isptr (force_ptr p) =  isptr p.
Proof.
intros. destruct p; reflexivity.
Qed.
#[export] Hint Rewrite isptr_force_ptr' : norm.

Ltac no_evars P := (has_evar P; fail 1) || idtac.

Create HintDb computable.
Inductive computable {t:Type} (x:t) : Prop := computable_any.

Ltac putable' x :=
 lazymatch x with
 | O => idtac
 | S ?x => putable x
 | Z.lt ?x ?y => putable x; putable y
 | Z.le ?x ?y => putable x; putable y
 | Z.gt ?x ?y => putable x; putable y
 | Z.ge ?x ?y => putable x; putable y
 | eq?x ?y => putable x; putable y
 | ?x <> ?y => putable x; putable y
 | Zpos ?x => putable x
 | Zneg ?x => putable x
 | Z0 => idtac
 | xH => idtac
 | xI ?x => putable x
 | xO ?x => putable x
 | Z.add ?x ?y => putable x; putable y
 | Z.sub ?x ?y => putable x; putable y
 | Z.mul ?x ?y => putable x; putable y
 | Z.div ?x ?y => putable x; putable y
 | Z.modulo ?x ?y => putable x; putable y
 | Z.max ?x ?y => putable x; putable y
 | Z.opp ?x => putable x
 | Ceq => idtac
 | Cne => idtac
 | Clt => idtac
 | Cle => idtac
 | Cgt => idtac
 | Cge => idtac
 | ?x /\ ?y => putable x; putable y
 | two_power_nat ?x => putable x
 | Int.eq ?x ?y => putable x; putable y
 | Int64.eq ?x ?y => putable x; putable y
 | Ptrofs.eq ?x ?y => putable x; putable y
 | Int.lt ?x ?y => putable x; putable y
 | Int64.lt ?x ?y => putable x; putable y
 | Ptrofs.lt ?x ?y => putable x; putable y
 | Int.ltu ?x ?y => putable x; putable y
 | Int64.ltu ?x ?y => putable x; putable y
 | Ptrofs.ltu ?x ?y => putable x; putable y
 | Int.add ?x ?y => putable x; putable y
 | Int64.add ?x ?y => putable x; putable y
 | Ptrofs.add ?x ?y => putable x; putable y
 | Int.sub ?x ?y => putable x; putable y
 | Int64.sub ?x ?y => putable x; putable y
 | Ptrofs.sub ?x ?y => putable x; putable y
 | Int.mul ?x ?y => putable x; putable y
 | Int64.mul ?x ?y => putable x; putable y
 | Ptrofs.mul ?x ?y => putable x; putable y
 | Int.neg ?x => putable x
 | Int64.neg ?x => putable x
 | Ptrofs.neg ?x => putable x
 | Int.cmp ?op ?x ?y => putable op; putable x; putable y
 | Int64.cmp ?op ?x ?y => putable op; putable x; putable y
 | Ptrofs.cmp ?op ?x ?y => putable op; putable x; putable y
 | Int.cmpu ?op ?x ?y => putable op; putable x; putable y
 | Int64.cmpu ?op ?x ?y => putable op; putable x; putable y
 | Ptrofs.cmpu ?op ?x ?y => putable op; putable x; putable y
 | Int.repr ?x => putable x
 | Int64.repr ?x => putable x
 | Ptrofs.repr ?x => putable x
 | Int.signed ?x => putable x
 | Int64.signed ?x => putable x
 | Ptrofs.signed ?x => putable x
 | Int.unsigned ?x => putable x
 | Int64.unsigned ?x => putable x
 | Ptrofs.unsigned ?x => putable x
 | two_power_nat ?x => putable x
 | Int.max_unsigned => idtac
 | Int64.max_unsigned => idtac
 | Ptrofs.max_unsigned => idtac
 | Int.min_signed => idtac
 | Int64.min_signed => idtac
 | Ptrofs.min_signed => idtac
 | Int.max_signed => idtac
 | Int64.max_signed => idtac
 | Ptrofs.max_signed => idtac
 | Int.modulus => idtac
 | Int64.modulus => idtac
 | Ptrofs.modulus => idtac
 | Int.zwordsize => idtac
 | Int64.zwordsize => idtac
 | Ptrofs.zwordsize => idtac
 | _ => tryif (let b := eval cbv delta [x] in x in putable b) then idtac else fail
end
with putable x :=
  first [putable' x
         | tryif (try (assert (computable x) by (clear; auto 100 with computable); fail 1)) then fail else idtac ].

#[export] Hint Extern 1 (computable ?x) => (putable' x; apply computable_any) : computable.

Ltac computable := match goal with |- ?x =>
 no_evars x;
 putable x;
 compute; clear; repeat split; auto; congruence;
  (match goal with |- context [Archi.ptr64] => idtac end;
    first [change Archi.ptr64 with false | change Archi.ptr64 with true];
    compute; repeat split; auto; congruence)
end.

Lemma sign_ext_range2:
   forall lo n i hi,
      0 < n < Int.zwordsize ->
      lo = - two_p (n-1) ->
      hi = two_p (n-1) - 1 ->
      lo <= Int.signed (Int.sign_ext n i) <= hi.
Proof.
intros.
subst.
pose proof (Int.sign_ext_range n i H).
lia.
Qed.

Lemma zero_ext_range2:
  forall n i lo hi,
      0 <= n < Int.zwordsize ->
      lo = 0 ->
      hi = two_p n - 1 ->
      lo <= Int.unsigned (Int.zero_ext n i) <= hi.
Proof.
intros; subst.
pose proof (Int.zero_ext_range n i H).
lia.
Qed.

#[export] Hint Extern 3 (_ <= Int.signed (Int.sign_ext _ _) <= _) =>
    (apply sign_ext_range2; [computable | reflexivity | reflexivity]) : core.

#[export] Hint Extern 3 (_ <= Int.unsigned (Int.zero_ext _ _) <= _) =>
    (apply zero_ext_range2; [computable | reflexivity | reflexivity]) : core.

#[export] Hint Rewrite sign_ext_inrange using assumption : norm.
#[export] Hint Rewrite zero_ext_inrange using assumption : norm.

Definition repable_signed_dec (z: Z) : {repable_signed z}+{~repable_signed z}.
Proof.
 intros. unfold repable_signed.
 destruct (zlt z Int.min_signed).
 right; intros [? _]; unfold Int.min_signed; lia.
 destruct (zlt Int.max_signed z).
 right; intros [_ ?]; unfold Int.max_signed; lia.
 left; split; lia.
Defined.

Lemma repable_signed_mult2:
  forall i j, i<>0 -> (j <= Int.max_signed \/ i <> -1) ->
   repable_signed (i*j) -> repable_signed j.
Proof.
intros until 1. intro HACK. intros.
assert (MAX: 0 < Int.max_signed) by (compute; auto).
assert (MIN: Int.min_signed < 0) by (compute; auto).
hnf in H0|-*.
assert (0 < i \/ i < 0) by lia; clear H.
destruct H1.
replace i with ((i-1)+1) in H0 by lia.
rewrite Z.mul_add_distr_r in H0.
rewrite Z.mul_1_l in H0.
assert (j < 0 \/ 0 <= j) by lia. destruct H1.
assert ((i-1)*j <= 0) by (apply Z.mul_nonneg_nonpos; lia).
lia.
assert (0 <= (i-1)*j) by (apply Z.mul_nonneg_nonneg; lia).
lia.
replace i with ((i+1)-1) in H0 by lia.
rewrite Z.mul_sub_distr_r in H0.
rewrite Z.mul_1_l in H0.
assert (MINMAX: Int.min_signed = -Int.max_signed - 1) by reflexivity.
assert (j < 0 \/ 0 <= j) by lia. destruct H1.
assert (0 <= (i+1)*j) by (apply Z.mul_nonpos_nonpos; lia).
rewrite MINMAX in H0|-*.
lia.
assert ((i+1)*j <= 0) by (apply Z.mul_nonpos_nonneg; lia).
rewrite MINMAX in H0|-*.
split; try lia.
clear MIN MINMAX.
destruct H0 as [? _].
assert (- Int.max_signed <= 1 + (i+1)*j - j) by lia; clear H0.
assert (-1 - (i + 1) * j + j <= Int.max_signed) by lia; clear H3.
destruct HACK; auto.
assert (i < -1) by lia.
destruct (zlt 0 j); try lia.
assert ((i+1)*j < 0).
rewrite Z.mul_add_distr_r.
replace i with ((i+1)-1) by lia.
rewrite Z.mul_sub_distr_r.
assert ((i+1)*j<0); [ | lia].
apply Z.mul_neg_pos; auto. lia.
lia.
Qed.

Lemma repable_signed_mult1:
  forall i j, j<>0 ->  (i <= Int.max_signed \/ j <> -1) ->
              repable_signed (i*j) -> repable_signed i.
Proof.
intros.
 rewrite Zmult_comm in H1.
 apply repable_signed_mult2 in H0; auto.
Qed.

Lemma force_signed_int_e:
  forall i, force_signed_int (Vint i) = Int.signed i.
Proof. reflexivity. Qed.
#[export] Hint Rewrite force_signed_int_e : norm.

Ltac const_equation x :=
  let y := eval compute in x
   in exact (x = y).

Ltac Zground X :=
  match X with
  | Z0 => idtac
  | Zpos ?y => Zground y
  | Zneg ?y => Zground y
  | xH => idtac
  | xO ?y => Zground y
  | xI ?y => Zground y
 end.

Ltac natground X :=
  match X with O => idtac | S ?Y => natground Y end.

Ltac compute_Z_of_nat :=
 repeat
  match goal with
  | H: context [Z.of_nat ?n] |- _ =>
          natground n;
          let z := constr:(Z.of_nat n) in let y := eval hnf in z
           in change z with y in *
  | |- context [Z.of_nat ?n] =>
          natground n;
          let z := constr:(Z.of_nat n) in let y := eval hnf in z
           in change z with y in *
   end.

(*
Ltac pose_const_equation X :=
 match goal with
 | H: X = ?Y |- _ => Zground Y
 | _ => let z := eval compute in X in assert (X = z) by reflexivity
 end.
*)

Ltac pose_const_equation X :=
 match goal with
 | H: X = ?Y |- _ => Zground Y
 | _ => let z := eval compute in X in
            match z with context C [Archi.ptr64] =>
                       first [
                           unify Archi.ptr64 false; let u := context C [false] in let u := eval compute in u in change X with u in *
                          |unify Archi.ptr64 true; let u := context C [true] in let u := eval compute in u in change X with u in *
                      ]
              | _ => change X with z in *
            end
 end.

Ltac perhaps_post_const_equation X :=
 lazymatch goal with
 | H: context [X] |- _ => pose_const_equation X
(* | H:= context [X] |- _ => pose_const_equation X *)
 | |- context [X] => pose_const_equation X
 | |- _ => idtac
 end.

Ltac pose_const_equations L :=
 match L with
 | ?X :: ?Y => perhaps_post_const_equation X; pose_const_equations Y
 | nil => idtac
 end.

Import ListNotations.

Ltac pose_standard_const_equations :=
pose_const_equations
  [
  Int.zwordsize; Int.modulus; Int.half_modulus; Int.max_unsigned; Int.max_signed; Int.min_signed;
  Int64.zwordsize; Int64.modulus; Int64.half_modulus; Int64.max_unsigned; Int64.max_signed; Int64.min_signed;
  Ptrofs.zwordsize; Ptrofs.modulus; Ptrofs.half_modulus; Ptrofs.max_unsigned; Ptrofs.max_signed; Ptrofs.min_signed;
  Byte.min_signed; Byte.max_signed; Byte.max_unsigned; Byte.modulus
  ];
 pose_const_equations [Int.wordsize; Int64.wordsize; Ptrofs.wordsize].

Ltac pose_lemma F A L :=
  match type of (L A) with ?T =>
     lazymatch goal with
      | H:  T |- _ => fail
      | H:  T /\ _ |- _ => fail
      | |- _ => pose proof (L A)
     end
  end.

Ltac pose_lemmas F L :=
 repeat
  match goal with
  | |- context [F ?A] => pose_lemma F A L
  | H: context [F ?A] |- _ => pose_lemma F A L
 end.

Ltac rep_lia_setup :=
 repeat match goal with
            | x := _ : ?T |- _ => lazymatch T with Z => fail | nat => fail | _ => clearbody x end
            end;
 zify;
  try autorewrite with rep_lia in *;
  unfold repable_signed in *;
  pose_Zlength_nonneg;
  pose_lemmas Byte.unsigned Byte.unsigned_range;
  pose_lemmas Byte.signed Byte.signed_range;
  pose_lemmas Int.unsigned Int.unsigned_range;
  pose_lemmas Int.signed Int.signed_range;
  pose_lemmas Int64.unsigned Int64.unsigned_range;
  pose_lemmas Int64.signed Int64.signed_range;
  pose_lemmas Ptrofs.unsigned Ptrofs.unsigned_range;
  pose_standard_const_equations.

Ltac rep_lia_setup2 := idtac.

Ltac rep_lia :=
   rep_lia_setup;
   rep_lia_setup2;
   lia.

Ltac repable_signed :=
  idtac "Warning: repable_signed is deprecated;  use rep_lia"; rep_lia.

Lemma Vubyte_injective i j (H: Vubyte i = Vubyte j): i=j.
Proof.
  assert (B: Byte.zwordsize = 8) by reflexivity.
  assert (I: Int.zwordsize = 32) by reflexivity.
  apply Byte.same_bits_eq; intros a A.
  unfold Vubyte in H. remember (Int.repr (Byte.unsigned i)) as z.
  inv H. destruct i; destruct j. unfold Byte.testbit.
  unfold Byte.unsigned in H1. simpl in *.
  rewrite <- 2 Int.testbit_repr, H1; trivial; lia.
Qed.

Lemma map_Vubyte_injective: forall l m, map Vubyte l = map Vubyte m -> l=m.
Proof. induction l; intros.
+ destruct m; simpl in *; inv H; trivial.
+ destruct m; [ inv H |]. rewrite 2 map_cons in H. apply cons_inv in H.
  destruct H; subst. apply Vubyte_injective in H. f_equal; eauto.
Qed.

Lemma Vbyte_injective a b (H: Vbyte a = Vbyte b): a=b.
Proof. unfold Vbyte in H. apply Vint_injective in H.
  apply Byte.same_bits_eq; intros i I.
  assert (Imin: Int.min_signed = -2147483648) by reflexivity.
  assert (Imax: Int.max_signed = 2147483647) by reflexivity.
  assert (Bmin: Byte.min_signed = -128) by reflexivity.
  assert (Bmax: Byte.max_signed = 127) by reflexivity.
  assert (Byte.signed a = Byte.signed b).
  { rewrite <- (Int.signed_repr (Byte.signed a)).
    rewrite <- (Int.signed_repr (Byte.signed b)).
    rewrite H; trivial. specialize (Byte.signed_range b); lia.
    specialize (Byte.signed_range a); lia. }
  clear H. unfold Byte.testbit. rewrite 2 Byte.unsigned_signed.
  unfold Byte.lt. rewrite H0. trivial.
Qed.

Lemma Znth_map_Vbyte: forall (i : Z) (l : list byte),
  0 <= i < Zlength l -> Znth i (map Vbyte l)  = Vbyte (Znth i l).
Proof.
  intros i l.
  apply Znth_map.
Qed.
#[export] Hint Rewrite Znth_map_Vbyte using old_list_solve : norm entailer_rewrite.

Lemma Znth_map_Vubyte: forall (i : Z) (l : list byte),
  0 <= i < Zlength l -> Znth i (map Vubyte l)  = Vubyte (Znth i l).
Proof.
  intros i l.
  apply Znth_map.
Qed.
#[export] Hint Rewrite Znth_map_Vubyte using old_list_solve : norm entailer_rewrite.

Lemma repr_inj_signed:
  forall i j,
    repable_signed i -> repable_signed j -> Int.repr i = Int.repr j -> i=j.
Proof.
intros.
rewrite <- (Int.signed_repr i) by rep_lia.
rewrite <- (Int.signed_repr j) by rep_lia.
congruence.
Qed.

Lemma repr_inj_unsigned:
  forall i j,
    0 <= i <= Int.max_unsigned ->
    0 <= j <= Int.max_unsigned ->
    Int.repr i = Int.repr j -> i=j.
Proof.
intros.
rewrite <- (Int.unsigned_repr i) by rep_lia.
rewrite <- (Int.unsigned_repr j) by rep_lia.
congruence.
Qed.

Lemma repr_inj_unsigned64:
  forall i j,
    0 <= i <= Int64.max_unsigned ->
    0 <= j <= Int64.max_unsigned ->
    Int64.repr i = Int64.repr j -> i=j.
Proof.
intros.
rewrite <- (Int64.unsigned_repr i) by rep_lia.
rewrite <- (Int64.unsigned_repr j) by rep_lia.
congruence.
Qed.

Lemma ptrofs_repr_inj_unsigned:
  forall i j,
    0 <= i <= Ptrofs.max_unsigned ->
    0 <= j <= Ptrofs.max_unsigned ->
    Ptrofs.repr i = Ptrofs.repr j -> i=j.
Proof.
intros.
rewrite <- (Ptrofs.unsigned_repr i) by rep_lia.
rewrite <- (Ptrofs.unsigned_repr j) by rep_lia.
congruence.
Qed.

Lemma repr_inj_signed':
  forall i j,
    (* The first two premises are not needed to prove this,
     but are used to limit its applicability *)
    repable_signed i -> repable_signed j ->
    Int.repr i <> Int.repr j -> i<>j.
Proof.
intros.
congruence.
Qed.

Lemma repr_inj_unsigned':
  forall i j,
    0 <= i <= Int.max_unsigned ->
    0 <= j <= Int.max_unsigned ->
    Int.repr i <> Int.repr j -> i<>j.
Proof.
intros.
congruence.
Qed.

Lemma opaque_constant {A: Type} (N: A) : {x: A | x=N}.
Proof. exists N. reflexivity. Qed.

Ltac hint := idtac "Hints are only available when verifying C programs,
that is, when VST.floyd.proofauto has been imported.  But you have
imported only VST.floyd.functional_base, without separation logic.

In VST.floyd.functional_base the following VST tactics are available:
rep_lia, list_solve, if_tac, autorewrite with sublist, computable, ...".

Lemma lt_repr64:
     forall i j : Z,
       repable_signed i ->
       repable_signed j ->
       Int64.lt (Int64.repr i) (Int64.repr j) = true -> (i < j)%Z.
Proof.
intros.
unfold Int64.lt in H1. if_tac in H1; inv H1.
rewrite !Int64.signed_repr in H2 by rep_lia.
auto.
Qed.

Lemma lt_repr_false:
     forall i j : Z,
       repable_signed i ->
       repable_signed j ->
       Int.lt (Int.repr i) (Int.repr j) = false -> (i >= j)%Z.
Proof.
intros.
unfold Int.lt in H1. if_tac in H1; inv H1.
rewrite !Int.signed_repr in H2 by rep_lia.
auto.
Qed.

Lemma lt_repr_false64:
     forall i j : Z,
       repable_signed i ->
       repable_signed j ->
       Int64.lt (Int64.repr i) (Int64.repr j) = false -> (i >= j)%Z.
Proof.
intros.
unfold Int64.lt in H1. if_tac in H1; inv H1.
rewrite !Int64.signed_repr in H2 by rep_lia.
auto.
Qed.

Lemma lt_inv:
 forall i j,
   Int.lt i j = true -> (Int.signed i < Int.signed j)%Z.
Proof.
intros.
unfold Int.lt in H. if_tac in H; inv H. auto.
Qed.

Lemma lt_inv64:
 forall i j,
   Int64.lt i j = true -> (Int64.signed i < Int64.signed j)%Z.
Proof.
intros.
unfold Int64.lt in H. if_tac in H; inv H. auto.
Qed.

Lemma lt_false_inv:
 forall i j,
   Int.lt i j = false -> (Int.signed i >= Int.signed j)%Z.
Proof.
intros.
unfold Int.lt in H. if_tac in H; inv H. auto.
Qed.

Lemma lt_false_inv64:
 forall i j,
   Int64.lt i j = false -> (Int64.signed i >= Int64.signed j)%Z.
Proof.
intros.
unfold Int64.lt in H. if_tac in H; inv H. auto.
Qed.

#[export] Hint Extern 2 (repable_signed ?i) =>
  (putable i; split; computable) : core.

Lemma divu_repr:
 forall i j,
  0 <= i <= Int.max_unsigned ->
  0 <= j <= Int.max_unsigned ->
  Int.divu (Int.repr i) (Int.repr j) = Int.repr (i / j).
Proof.
intros.
unfold Int.divu.
rewrite !Int.unsigned_repr; auto.
Qed.

Lemma divu_repr64:
 forall i j,
  0 <= i <= Int64.max_unsigned ->
  0 <= j <= Int64.max_unsigned ->
  Int64.divu (Int64.repr i) (Int64.repr j) = Int64.repr (i / j).
Proof.
intros.
unfold Int64.divu.
rewrite !Int64.unsigned_repr; auto.
Qed.

Lemma ptrofs_divu_repr:
 forall i j,
  0 <= i <= Ptrofs.max_unsigned ->
  0 <= j <= Ptrofs.max_unsigned ->
  Ptrofs.divu (Ptrofs.repr i) (Ptrofs.repr j) = Ptrofs.repr (i / j).
Proof.
intros.
unfold Ptrofs.divu.
rewrite !Ptrofs.unsigned_repr; auto.
Qed.

#[export] Hint Rewrite divu_repr divu_repr64 ptrofs_divu_repr
          using rep_lia : norm.

author: PrincetonUniversity

repo: VST


text:
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require list.Length.
Require int.Int.
Require list.Mem.
Require list.Append.

(* Why3 assumption *)
Definition unit := unit.

Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.

(* Why3 assumption *)
Inductive regexp :=
  | Empty : regexp
  | Epsilon : regexp
  | Char : char -> regexp
  | Alt : regexp -> regexp -> regexp
  | Concat : regexp -> regexp -> regexp
  | Star : regexp -> regexp.
Axiom regexp_WhyType : WhyType regexp.
Existing Instance regexp_WhyType.

(* Why3 assumption *)
Definition word := (list char).

(* Why3 assumption *)
Inductive mem : (list char) -> regexp -> Prop :=
  | mem_eps : (mem nil Epsilon)
  | mem_char : forall (c:char), (mem (cons c nil) (Char c))
  | mem_altl : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem w r1) ->
      (mem w (Alt r1 r2))
  | mem_altr : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem w r2) ->
      (mem w (Alt r1 r2))
  | mem_concat : forall (w1:(list char)) (w2:(list char)) (r1:regexp)
      (r2:regexp), (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2)
      (Concat r1 r2)))
  | mems1 : forall (r:regexp), (mem nil (Star r))
  | mems2 : forall (w1:(list char)) (w2:(list char)) (r:regexp), (mem w1
      r) -> ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).

Axiom inversion_mem_star_gen : forall (c:char) (w:(list char)) (r:regexp)
  (w':(list char)) (r':regexp), ((w' = (cons c w)) /\ (r' = (Star r))) ->
  ((mem w' r') -> exists w1:(list char), exists w2:(list char),
  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).

Axiom inversion_mem_star : forall (c:char) (w:(list char)) (r:regexp), (mem
  (cons c w) (Star r)) -> exists w1:(list char), exists w2:(list char),
  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 (Star r))).

(* Why3 goal *)
Theorem WP_parameter_residual : forall (r:regexp) (c:char),
  match r with
  | Empty => True
  | Epsilon => True
  | (Char c') => True
  | (Alt r1 r2) => True
  | (Concat r1 r2) => True
  | (Star r1) => forall (o:regexp), (forall (w:(list char)), (mem w o) <->
      (mem (cons c w) r1)) -> forall (w:(list char)), (mem w (Concat o
      r)) <-> (mem (cons c w) r)
  end.
(* Why3 intros r c. *)
intros r c.
destruct r; auto.
intros.
split; intros.

inversion H0; subst; clear H0.
rewrite List.app_comm_cons.
constructor; auto.
rewrite <- H; auto.

destruct (inversion_mem_star _ _ _ H0) as (w1 & w2 & h1 & h2 & h3).
subst w.
constructor; auto.
now rewrite H.

Qed.

author: kit-ty-kate


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(***********************************************************************
    Proof of Bertrand's conjecture: Raux.v
                                         Laurent.Thery@inria.fr (2002)
  *********************************************************************)

From Coq Require Export Arith.
From Coq Require Import ZArith Classical_Prop.
From Coq Require Import Rbase Rfunctions Ranalysis Rtrigo.
From Coq Require Export Rpower.
From Bertrand Require Export Misc Div.

#[export] Hint Resolve exp_pos: real.
#[export] Hint Resolve exp_increasing: real.
#[export] Hint Resolve ln_increasing: real.
#[export] Hint Resolve sqrt_lt_R0: real.
#[export] Hint Resolve Rmult_lt_0_compat: real.
#[export] Hint Resolve Rplus_lt_compat_l: real.
#[export] Hint Resolve Rinv_0_lt_compat: real.
#[export] Hint Resolve Rlt_not_eq: real.

(** Axuillary properties of reals functions *)

Theorem Rlt_Rminus_ZERO : forall r1 r2 : R, (r2 < r1)%R -> (0 < r1 - r2)%R.
Proof.
intros r1 r2 H; replace 0%R with (r1 - r1)%R; unfold Rminus in |- *;
 auto with real.
Qed.
#[export] Hint Resolve Rlt_Rminus_ZERO: real.

Theorem P_Rmin : forall (P : R -> Prop) (x y : R), P x -> P y -> P (Rmin x y).
Proof.
intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); auto.
Qed.

Theorem Rle_pow :
 forall (e : R) (n m : nat), (1 < e)%R -> n <= m -> (e ^ n <= e ^ m)%R.
Proof.
intros e n m H H0; case (proj1 (Nat.lt_eq_cases _ _) H0); auto with real.
intros H1; rewrite H1; auto with real.
Qed.

Theorem Rle_square :
 forall x y : R, (0 <= x)%R -> (0 <= y)%R -> (x * x <= y * y)%R -> (x <= y)%R.
Proof.
intros x y H H0 H1; case (Rle_or_lt x y); auto.
intros H2; Contradict H1; apply Rlt_not_le.
apply Rle_lt_trans with (x * y)%R; auto with real.
apply Rmult_lt_compat_l; auto with arith.
apply Rle_lt_trans with (1 := H0); auto.
Qed.

Theorem sqr_Rsqrt : forall n : nat, (INR (sqr n) <= sqrt (INR n))%R.
Proof.
intros n; apply Rle_square; auto with real.
apply sqrt_positivity; replace 0%R with (INR 0); auto with real arith.
rewrite <- sqrt_mult; try rewrite sqrt_square; auto with real.
rewrite <- mult_INR; apply le_INR.
apply sqr_le.
Qed.

Theorem div_Rdiv :
 forall n m : nat, 0 < m -> (INR (div n m) <= INR n / INR m)%R.
Proof.
intros n m H; apply Rmult_le_reg_l with (r := INR m); auto with real.
replace (INR m * (INR n / INR m))%R with (INR n).
rewrite <- mult_INR; apply le_INR; auto with arith.
apply div_le; auto.
unfold Rdiv in |- *.
replace (INR m * (INR n * / INR m))%R with (INR n * (INR m * / INR m))%R;
 [ rewrite Rinv_r | ring ]; auto with real.
Qed.

Theorem Rpower_pow :
 forall (n : nat) (x : R), (0 < x)%R -> Rpower x (INR n) = (x ^ n)%R.
Proof.
intros n; elim n; simpl in |- *; auto; fold INR in |- *.
intros x H; apply Rpower_O; auto.
intros n1; case n1.
intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto.
intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1;
 auto with real.
Qed.

Theorem INR_power : forall n m : nat, INR (power n m) = (INR n ^ m)%R.
Proof.
intros n m; elim m; simpl in |- *; auto with real.
intros m1 H; rewrite mult_INR; rewrite H; auto.
Qed.

Theorem Rlt_increasing :
 forall (f f' : R -> R) (a b : R),
 (a <= b)%R ->
 (forall x : R, (a <= x)%R -> (x <= b)%R -> derivable_pt_lim f x (f' x)) ->
 (forall x : R, (a <= x)%R -> (x <= b)%R -> (0 <= f' x)%R) ->
 (0 < f a)%R -> (0 < f b)%R.
Proof.
intros f f' a b H H0 H1 H2.
case (Rtotal_order a b); intros H'2.
case (MVT_cor2 f f' a b); auto.
intros c (H3, H4); auto.
intros c (H3, (H4, H5)).
replace (f b) with (f a + (f b - f a))%R; [ rewrite H3 | ring ].
apply Rplus_lt_le_0_compat; auto with real.
apply Rmult_le_pos; auto with real.
case H'2; intros H'3.
rewrite <- H'3; auto.
Contradict H'3; auto with real.
unfold Rgt in |- *; apply Rle_not_lt; auto.
Qed.

author: coq-community

repo: bertrand

save_path: github-repos/coq/coq-community-bertrand


text:
From Perennial.program_proof Require Import grove_prelude.
From Goose.github_com.mit_pdos.gokv Require Export mpaxos.
From Perennial.program_proof Require Import marshal_stateless_proof.

Module applyAsFollowerArgs.
Section applyAsFollowerArgs.
Context `{!heapGS Σ}.

Record C :=
mkC {
  epoch : u64 ;
  nextIndex : u64 ;
  state : list u8 ;
}.

Definition has_encoding (encoded:list u8) (args:C) : Prop :=
  encoded = (u64_le args.(epoch)) ++ (u64_le args.(nextIndex)) ++ args.(state).

Context `{!heapGS Σ}.

Definition own args_ptr args : iProp Σ :=
  ∃ state_sl,
  "#Hargs_epoch" ∷ readonly (args_ptr ↦[mpaxos.applyAsFollowerArgs :: "epoch"] #args.(epoch)) ∗
  "#Hargs_index" ∷ readonly (args_ptr ↦[mpaxos.applyAsFollowerArgs :: "nextIndex"] #args.(nextIndex)) ∗
  "#Hargs_state" ∷ readonly (args_ptr ↦[mpaxos.applyAsFollowerArgs :: "state"] (slice_val state_sl)) ∗
  "#Hargs_state_sl" ∷ readonly (is_slice_small state_sl byteT 1 args.(state))
  .

Lemma wp_Encode (args_ptr:loc) (args:C) :
  {{{
        own args_ptr args
  }}}
    mpaxos.encodeApplyAsFollowerArgs #args_ptr
  {{{
        enc enc_sl, RET (slice_val enc_sl);
        ⌜has_encoding enc args⌝ ∗
        is_slice enc_sl byteT 1 enc
  }}}.
Admitted.

Lemma wp_Decode enc enc_sl (args:C) :
  {{{
        ⌜has_encoding enc args⌝ ∗
        is_slice_small enc_sl byteT 1 enc
  }}}
    mpaxos.decodeApplyAsFollowerArgs (slice_val enc_sl)
  {{{
        args_ptr, RET #args_ptr; own args_ptr args
  }}}.
Admitted.

End applyAsFollowerArgs.
End applyAsFollowerArgs.

Module applyAsFollowerReply.
Section applyAsFollowerReply.
Context `{!heapGS Σ}.

Record C :=
mkC {
  err: u64 ;
}.

Definition has_encoding (encoded:list u8) (reply:C) : Prop :=
  encoded = (u64_le reply.(err)).

Context `{!heapGS Σ}.

Definition own reply_ptr reply q : iProp Σ :=
  "Hreply_err" ∷ reply_ptr ↦[mpaxos.applyAsFollowerReply :: "err"]{q} #reply.(err)
  .

Lemma wp_Encode (reply_ptr:loc) (reply:C) q :
  {{{
        own reply_ptr reply q
  }}}
    mpaxos.encodeApplyAsFollowerReply #reply_ptr
  {{{
        enc enc_sl, RET (slice_val enc_sl);
        ⌜has_encoding enc reply⌝ ∗
        is_slice enc_sl byteT 1 enc
  }}}.
Admitted.

Lemma wp_Decode enc enc_sl (reply:C) :
  {{{
        ⌜has_encoding enc reply⌝ ∗
        is_slice_small enc_sl byteT 1 enc
  }}}
    mpaxos.decodeApplyAsFollowerReply (slice_val enc_sl)
  {{{
        reply_ptr, RET #reply_ptr; own reply_ptr reply 1
  }}}.
Admitted.

End applyAsFollowerReply.
End applyAsFollowerReply.

Module applyReply.
Section applyReply.
Context `{!heapGS Σ}.

Record C :=
mkC {
  err: u64 ;
  ret: list u8 ;
}.

Definition has_encoding (encoded:list u8) (args:C) : Prop :=
  encoded = (u64_le args.(err)) ++ args.(ret).

Context `{!heapGS Σ}.

Definition own args_ptr args q : iProp Σ :=
  ∃ ret_sl,
  "Hreply_epoch" ∷ args_ptr ↦[mpaxos.applyReply :: "err"]{q} #args.(err) ∗
  "Hreply_ret" ∷ args_ptr ↦[mpaxos.applyReply :: "ret"]{q} (slice_val ret_sl) ∗
  "Hreply_ret_sl" ∷ is_slice_small ret_sl byteT q args.(ret)
  .

Lemma wp_Encode (args_ptr:loc) (args:C) q :
  {{{
        own args_ptr args q
  }}}
    mpaxos.encodeApplyReply #args_ptr
  {{{
        enc enc_sl, RET (slice_val enc_sl);
        ⌜has_encoding enc args⌝ ∗
        is_slice enc_sl byteT 1 enc
  }}}.
Admitted.

Lemma wp_Decode enc enc_sl (args:C) :
  {{{
        ⌜has_encoding enc args⌝ ∗
        is_slice_small enc_sl byteT 1 enc
  }}}
    mpaxos.decodeApplyReply (slice_val enc_sl)
  {{{
        args_ptr, RET #args_ptr; own args_ptr args 1
  }}}.
Admitted.

End applyReply.
End applyReply.

Module enterNewEpochArgs.
Section enterNewEpochArgs.
Context `{!heapGS Σ}.

Record C :=
mkC {
  epoch: u64 ;
}.

Definition has_encoding (encoded:list u8) (args:C) : Prop :=
  encoded = (u64_le args.(epoch)).

Context `{!heapGS Σ}.

Definition own args_ptr args q : iProp Σ :=
  "Hargs_epoch" ∷ args_ptr ↦[mpaxos.enterNewEpochArgs :: "epoch"]{q} #args.(epoch)
  .

Lemma wp_Encode (args_ptr:loc) (args:C) q :
  {{{
        own args_ptr args q
  }}}
    mpaxos.encodeEnterNewEpochArgs #args_ptr
  {{{
        enc enc_sl, RET (slice_val enc_sl);
        ⌜has_encoding enc args⌝ ∗
        is_slice enc_sl byteT 1 enc
  }}}.
Admitted.

Lemma wp_Decode enc enc_sl (args:C) :
  {{{
        ⌜has_encoding enc args⌝ ∗
        is_slice_small enc_sl byteT 1 enc
  }}}
    mpaxos.decodeEnterNewEpochArgs (slice_val enc_sl)
  {{{
        args_ptr, RET #args_ptr; own args_ptr args 1
  }}}.
Admitted.

End enterNewEpochArgs.
End enterNewEpochArgs.

Module enterNewEpochReply.
Section enterNewEpochReply.
Context `{!heapGS Σ}.

Record C :=
mkC {
  err: u64 ;
  acceptedEpoch: u64 ;
  nextIndex: u64 ;
  state: list u8;
}.

Definition has_encoding (encoded:list u8) (args:C) : Prop :=
  encoded = (u64_le args.(err)) ++ (u64_le args.(acceptedEpoch)) ++ (u64_le args.(nextIndex))  ++ args.(state).

Context `{!heapGS Σ}.

Definition own args_ptr args q : iProp Σ :=
  ∃ state_sl,
  "Hreply_err" ∷ args_ptr ↦[mpaxos.enterNewEpochReply :: "err"]{q} #args.(err) ∗
  "Hreply_nextIndex" ∷ args_ptr ↦[mpaxos.enterNewEpochReply :: "nextIndex"]{q} #args.(nextIndex) ∗
  "Hreply_acceptedEpoch" ∷ args_ptr ↦[mpaxos.enterNewEpochReply :: "acceptedEpoch"]{q} #args.(acceptedEpoch) ∗
  "Hreply_ret" ∷ args_ptr ↦[mpaxos.enterNewEpochReply :: "state"]{q} (slice_val state_sl) ∗
  "Hreply_ret_sl" ∷ readonly (is_slice_small state_sl byteT 1 args.(state))
.

Lemma wp_Encode (args_ptr:loc) (args:C) q :
  {{{
        own args_ptr args q
  }}}
    mpaxos.encodeEnterNewEpochReply #args_ptr
  {{{
        enc enc_sl, RET (slice_val enc_sl);
        ⌜has_encoding enc args⌝ ∗
        is_slice enc_sl byteT 1 enc
  }}}.
Admitted.

Lemma wp_Decode enc enc_sl (args:C) :
  {{{
        ⌜has_encoding enc args⌝ ∗
        is_slice_small enc_sl byteT 1 enc
  }}}
    mpaxos.decodeEnterNewEpochReply (slice_val enc_sl)
  {{{
        args_ptr, RET #args_ptr; own args_ptr args 1
  }}}.
Admitted.

Global Instance enterNewEpochReply_fractional args_ptr args :
  fractional.Fractional (λ q : Qp, own args_ptr args q).
Proof.
  rewrite /own.
  unfold fractional.Fractional.
  iIntros.
  iSplit.
  {
    iIntros "H". iDestruct "H" as (?) "H".
    admit.
  }
  admit.
Admitted.

Global Instance enterNewEpochReply_as_fractional args_ptr args q :
  fractional.AsFractional (own args_ptr args q) (λ q : Qp, own args_ptr args q) q.
Proof.
  split; auto; apply _.
Qed.

(* FIXME: *)
Global Instance enterNewEpochReply_as_mapsto args_ptr args :
  AsMapsTo (own args_ptr args 1) (λ q : Qp, own args_ptr args q).
Proof.
(*   constructor; auto; intros; apply _. *)
Admitted.

End enterNewEpochReply.
End enterNewEpochReply.

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


text:
From SepLogic Require Import Pred Tactics Cancel.

Import PredNotations.

Theorem pred_impl_test1 (p1 p2: pred nat bool) m :
  (p1 * p2)%pred m ->
  (p2 * p1)%pred m.
Proof.
  intros.
  pred_impl.
  cancel.
Qed.

Theorem pred_iff_test1 (p1 p2: pred nat bool) m :
  (p1 * p2)%pred m ->
  (p2 * p1)%pred m.
Proof.
  intros.
  pred_iff.
  cancel.
Qed.

author: tchajed

repo: coq-sep-logic

save_path: github-repos/coq/tchajed-coq-sep-logic


text:
From Ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

(* motivating example *)

Goal forall n, n + n = 2 * n.
Show Proof.
elim.
  Show Proof.
  rewrite addn0.
  rewrite muln0.
  done.
Show Proof.
move=> n IH.
rewrite addSn.
rewrite addnS.
rewrite IH.
rewrite mulnS.
rewrite -addn2.
rewrite addnC.
done.
Show Proof.
Qed.

Print nat.

Print nat_rect.
Print nat_rect.

Definition mynat_ind_proof := fun (P : nat -> Prop) (f : P 0) (f0 : forall n : nat, P n -> P n.+1) =>
fix F (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 => f
  | n0.+1 => f0 n0 (F n0)
  end.

Lemma mynat_ind : forall (P : nat -> Prop), P 0 ->
  (forall n : nat, P n -> P n.+1) ->
  forall n, P n.
exact mynat_ind_proof.
Qed.

(* le vs. leq *)

Print le.
Print leq.

Goal forall n, 0 <= n.
done.
Show Proof.
Qed.

(* compare with: *)
Print Le.le_0_n.

Goal forall n m, n.+1 <= m.+1 -> n <= m.
done.
Show Proof.
Qed.

(* compare with: *)
Print le_S_n.
Print le_pred.

Goal forall n, n <= n.
done.
Qed.

Goal forall n, n <= n.+1.
done.
Qed.

Goal forall n, n < n = false.
by elim.
Qed.

(* 加算の可換性: prove in one line (without using addnC of course) *)

Lemma exo24 n m : m + n = n + m.
Proof.
Abort.

Lemma exo25 (u : nat -> nat) (u0 : u 0 = 2) (u1 : u 1 = 3) (un : forall n, u n.+2 = 3 * u n.+1 - 2 * u n) n :
  u n = 1 + 2 ^ n.
Proof.
Fail elim/yet_another_ind : n. (* see tactics_example.v *)
Abort.

Lemma exo26 d (Hd : odd d) : d.-1./2 = d./2.
Proof.
Abort.

Lemma exo27 d (Hd : ~~ odd d) : (d.-1)./2 = d./2.-1.
Proof.
Abort.

(* about leqP *)

Goal forall n : nat, (n <= 5 \/ 5 < n)%coq_nat.
move=> n.
destruct (Compare_dec.le_gt_dec n 5).
(* NB: does not replace n <= 5 with True *)
auto.
auto.
Show Proof.
Qed.

Goal forall n : nat, (n <= 5) || (5 < n).
move=> n.
case H : (n <= 5).
done.
move/negbT : H.
rewrite -ltnNge.
move=> ->.
done.
(* pros: replace (n <= 5) by true, etc.
   cons: rewrite in the 2nd branch because of mismatch with standard library,
     does not scale to three way case analysis *)
Qed.

Goal forall n : nat, (n <= 5) || (5 < n).
move=> n.
case: (leqP n 5).
done.
done.
Qed.

Definition rgb := sum unit bool.
Definition red : rgb := inl tt.
Definition green : rgb := inr false.
Definition blue : rgb := inr true.

Definition shift (c : rgb) : rgb :=
  match c with
  | inl _ => green
  | inr false => blue
  | inr true => red
  end.

(* Prove the following: *)
Lemma exo28 c : shift (shift (shift c)) = c.
Proof.
Abort.

CoInductive rgb_spec : rgb -> bool -> bool -> bool -> Prop :=
| red_spec : rgb_spec red true false false
| green_spec : rgb_spec green false true false
| blue_spec : rgb_spec blue false false true.

(* Prove the following: *)
Lemma exo29 (*rgbP*) c : rgb_spec c (c == red) (c == green) (c == blue).
Proof.
Admitted.

(* same as above but this time using rgbP: *)
Lemma exo30 c : shift (shift (shift c)) = c.
Proof.
Abort.

author: affeldt


text:
Require Import   Algebra.SetoidCat Algebra.Monoid.

Require Import RelationClasses Relation_Definitions Morphisms SetoidClass.

Section NearSemiRing.

  Context
    {A : Type}
    {SA : Setoid A}.

  Class NearSemiRing : Type :=
    {
      one : A;
      zero : A;
      times : SA ~> SA ~~> SA;
      plus : SA ~> SA ~~> SA;
      times_left_unit : forall a, times @ one @ a == a;
      times_right_unit : forall a, times @ a @ one == a;
      times_associativity : forall a b c, times @ (times @ a @ b) @ c == times @ a @ (times @ b @ c);
      plus_left_unit : forall a, plus @ zero @ a == a;
      plus_right_unit : forall a, plus @ a @ zero == a;
      plus_associativity : forall a b c, plus @ (plus @ a @ b) @ c == plus @ a @ (plus @ b @ c);
      times_left_absorb : forall a, times @ zero @ a == zero;
      times_left_distributivity : forall a b c, times @ (plus @ a @ b) @ c == plus @ (times @ a @ c) @ (times @ b @ c)
    }.

End NearSemiRing.

author: xu-hao

repo: CertifiedQueryArrow


text:
(*************************************************************************)
(* Copyright (C) 2013 - 2015                                             *)
(* Author C. Cohen                                                       *)
(* DRAFT - PLEASE USE WITH CAUTION                                       *)
(* License CeCILL-B                                                      *)
(*************************************************************************)

From mathcomp
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import choice path finset finfun fintype bigop.

Require Import finmap.

(*****************************************************************************)
(* This file provides a representation of multisets based on fsfun         *)
(*****************************************************************************)

Delimit Scope mset_scope with mset.
Local Open Scope fset_scope.
Local Open Scope fmap_scope.
Local Open Scope mset_scope.
Local Open Scope nat_scope.

Definition multiset (T : choiceType) := {fsfun _ : T => 0 : nat}.
Definition multiset_of (T : choiceType) of phant T := @multiset T.
Notation "'{mset' T }" := (@multiset_of _ (Phant T))
  (format "'{mset'  T }") : mset_scope.

Notation "[ 'mset' & key | x 'in' aT => F ]" := ([fsfun & key | x in aT => F ] : {mset _})
  (at level 0, x ident, only parsing) : mset_scope.
Notation "[ 'mset' x 'in' aT => F ]" := ([fsfun x in aT => F ] : {mset _})
  (at level 0, x ident, format "[ 'mset'  x  'in'  aT  =>  F ]") : mset_scope.

Identity Coercion multiset_multiset_of : multiset_of >-> multiset.
Coercion fset_of_multiset (T : choiceType) (A : multiset T) : finSet T :=
  domf (fmap_of_fsfun A).
Canonical multiset_predType (K : choiceType) :=  Eval hnf in mkPredType
  (@pred_of_finset K \o @fset_of_multiset K : multiset K -> pred K).
Canonical mset_finpredType (T: choiceType) :=
  mkFinPredType (multiset T) (fun _ _ => erefl).

Section MultisetOps.

Context {K : choiceType}.
Implicit Types (a b c : K) (A B C D : {mset K}) (s : seq K).

Definition mset0 : {mset K} := [fsfun].

Fact msetn_key : unit. Proof. exact: tt. Qed.
Definition msetn n a := [mset & msetn_key | x in [fset a] => n].

Fact seq_mset_key : unit. Proof. exact: tt. Qed.
Definition seq_mset (s : seq K) :=
  [mset & seq_mset_key | x in seq_fset s => count (pred1 x) s].

Fact msetU_key : unit. Proof. exact: tt. Qed.
Definition msetU A B := [mset & msetU_key | x in A `|` B => maxn (A x) (B x)].

Fact msetI_key : unit. Proof. exact: tt. Qed.
Definition msetI A B := [mset & msetI_key | x in A `|` B => minn (A x) (B x)].

Fact msetD_key : unit. Proof. exact: tt. Qed.
Definition msetD A B := [mset & msetD_key | x in A `|` B => A x + B x].

Fact msetB_key : unit. Proof. exact: tt. Qed.
Definition msetB A B := [mset & msetB_key | x in A `|` B => A x - B x].

Fact msetM_key : unit. Proof. exact: tt. Qed.
Definition msetM A B := [mset & msetM_key | x in A `*` B => A x.1 * B x.2].

Definition msubset A B := [forall x : A, A (val x) <= B (val x)].

Definition mproper A B := msubset A B && ~~ msubset B A.

Definition mdisjoint A B := (msetI A B == mset0).

End MultisetOps.

Notation "[ 'mset' a ]" := (msetn 1 a)
  (at level 0, a at level 99, format "[ 'mset'  a ]") : mset_scope.
Notation "[ 'mset' a : T ]" := [mset (a : T)]
  (at level 0, a at level 99, format "[ 'mset'  a   :  T ]") : mset_scope.
Notation "A `|` B" := (msetU A B) : mset_scope.
Notation "A `+` B" := (msetD A B) : mset_scope.
Notation "A `\` B" := (msetB A B) : mset_scope.
Notation "A `\ a" := (A `\` [mset a]) : mset_scope.
Notation "a |` A" := ([mset (a)] `|` A) : mset_scope.
Notation "a +` A" := ([mset (a)] `+` A) : mset_scope.
Notation "A `*` B" := (msetM A B) : mset_scope.

Notation "A `<=` B" := (msubset A B)
  (at level 70, no associativity) : mset_scope.

Notation "A `<` B" := (mproper A B)
  (at level 70, no associativity) : mset_scope.

(* This is left-associative due to historical limitations of the .. Notation. *)
Notation "[ 'mset' a1 ; a2 ; .. ; an ]" :=
  (msetD .. (a1 +` (msetn 1 a2)) .. (msetn 1 an))
  (at level 0, a1 at level 99,
   format "[ 'mset'  a1 ;  a2 ;  .. ;  an ]") : mset_scope.
Notation "A `&` B" := (msetI A B) : mset_scope.

Section MSetTheory.

Context {K : choiceType}.
Implicit Types (a b c : K) (A B C D : {mset K}) (s : seq K).

Lemma msetP {A B} : A =1 B <-> A = B.
Proof. exact: fsfunP. Qed.

Lemma in_mset a A : (a \in A) = (A a > 0).
Proof. by rewrite mem_finsupp lt0n. Qed.

Lemma mset_neq0 a A : (A a != 0) = (a \in A).
Proof. by rewrite mem_finsupp. Qed.

Lemma mset_eq0 a A : (A a == 0) = (a \notin A).
Proof. by rewrite mem_finsupp negbK. Qed.

Lemma mset_eq0P {a A} : reflect (A a = 0) (a \notin A).
Proof. by rewrite -mset_eq0; apply: eqP. Qed.

Lemma mset_gt0 a A : (A a > 0) = (a \in A).
Proof. by rewrite mem_finsupp lt0n. Qed.

Lemma mset_eqP {A B} : reflect (A =1 B) (A == B).
Proof. exact: (equivP eqP (iff_sym msetP)). Qed.

Lemma mset0E a : mset0 a = 0.
Proof. by rewrite /mset0 fsfunE. Qed.

Lemma msetnE n a b : (msetn n a) b = if b == a then n else 0.
Proof. by rewrite fsfunE inE. Qed.

Lemma msetnxx n a : (msetn n a) a = n. Proof. by rewrite msetnE eqxx. Qed.

Lemma msetE2 A B a :
 ((A `+` B) a = A a + B a) * ((A `|` B) a = maxn (A a) (B a))
* ((A `&` B) a = minn (A a) (B a)) * ((A `\` B) a = (A a) - (B a)).
Proof.
rewrite !fsfunE !inE -!mset_neq0; case: ifPn => //.
by rewrite negb_or !negbK => /andP [/eqP-> /eqP->].
Qed.

Lemma mset_seqE s a : (seq_mset s) a = count (pred1 a) s.
Proof. by rewrite fsfunE seq_fsetE; case: ifPn => // /count_memPn ->. Qed.

Lemma msetME A B (u : K * K) : (A `*` B) u = A u.1 * B u.2.
Proof.
rewrite !fsfunE inE; case: ifPn => //=.
by rewrite negb_and !memNfinsupp => /orP [] /eqP->; rewrite ?muln0.
Qed.

Lemma mset1DE a A b : (a +` A) b = (b == a) + A b.
Proof. by rewrite msetE2 msetnE; case: (b == a). Qed.

Lemma mset1UE a A b : (a |` A) b = maxn (b == a) (A b).
Proof. by rewrite msetE2 msetnE; case: (b == a). Qed.

Lemma msetB1E a A b : (A `\ a) b = (A b) - (b == a).
Proof. by rewrite msetE2 msetnE; case: (b == a). Qed.

Let msetE := (mset0E, msetE2, msetnE, msetnxx,
              mset1DE, mset1UE, msetB1E,
              mset_seqE, msetME).

Lemma in_mset0 a : a \in mset0 = false.
Proof. by rewrite in_mset !msetE. Qed.

Lemma in_msetn n a' a : a \in msetn n a' = (n > 0) && (a == a').
Proof. by rewrite in_mset msetE; case: (a == a'); rewrite ?andbT ?andbF. Qed.

Lemma in_mset1 a' a : a \in [mset a'] = (a == a').
Proof. by rewrite in_mset msetE; case: (a == _). Qed.

Lemma in_msetD A B a : (a \in A `+` B) = (a \in A) || (a \in B).
Proof. by rewrite !in_mset !msetE addn_gt0. Qed.

Lemma in_msetU A B a : (a \in A `|` B) = (a \in A) || (a \in B).
Proof. by rewrite !in_mset !msetE leq_max. Qed.

Lemma in_msetDU A B a : (a \in A `+` B) = (a \in A `|` B).
Proof. by rewrite in_msetU in_msetD. Qed.

Lemma in_msetI A B a : (a \in A `&` B) = (a \in A) && (a \in B).
Proof. by rewrite !in_mset msetE leq_min. Qed.

Lemma in_msetB A B a : (a \in A `\` B) = (B a < A a).
Proof. by rewrite -mset_neq0 msetE subn_eq0 ltnNge. Qed.

Lemma in_mset1U a' A a : (a \in a' |` A) = (a == a') || (a \in A).
Proof. by rewrite in_msetU in_mset msetE; case: (_ == _). Qed.

Lemma in_mset1D a' A a : (a \in a' +` A) = (a == a') || (a \in A).
Proof. by rewrite in_msetDU in_mset1U. Qed.

Lemma in_msetB1 A b a : (a \in A `\ b) = ((a == b) ==> (A a > 1)) && (a \in A).
Proof.
by rewrite in_msetB msetE in_mset; case: (_ == _); rewrite -?geq_max.
Qed.

Lemma in_msetM A B (u : K * K) : (u \in A `*` B) = (u.1 \in A) && (u.2 \in B).
Proof. by rewrite !mem_finsupp msetE muln_eq0 negb_or. Qed.

Definition in_msetE :=
  (in_mset0, in_mset1, in_msetn,
   in_mset1U, in_mset1D, in_msetB1,
   in_msetU, in_msetI, in_msetD, in_msetM
  ).

Let inE := (inE, in_msetE).

Lemma msetDC (A B : {mset K}) : A `+` B = B `+` A.
Proof. by apply/msetP=> a; rewrite !msetE addnC. Qed.

Lemma msetIC (A B : {mset K}) : A `&` B = B `&` A.
Proof. by apply/msetP=> a; rewrite !msetE minnC. Qed.

Lemma msetUC (A B : {mset K}) : A `|` B = B `|` A.
Proof. by apply/msetP => a; rewrite !msetE maxnC. Qed.

(* intersection *)

Lemma mset0I A : mset0 `&` A = mset0.
Proof. by apply/msetP => x; rewrite !msetE min0n. Qed.

Lemma msetI0 A : A `&` mset0 = mset0.
Proof. by rewrite msetIC mset0I. Qed.

Lemma msetIA A B C : A `&` (B `&` C) = A `&` B `&` C.
Proof. by apply/msetP=> x; rewrite !msetE minnA. Qed.

Lemma msetICA A B C : A `&` (B `&` C) = B `&` (A `&` C).
Proof. by rewrite !msetIA (msetIC A). Qed.

Lemma msetIAC A B C : A `&` B `&` C = A `&` C `&` B.
Proof. by rewrite -!msetIA (msetIC B). Qed.

Lemma msetIACA A B C D : (A `&` B) `&` (C `&` D) = (A `&` C) `&` (B `&` D).
Proof. by rewrite -!msetIA (msetICA B). Qed.

Lemma msetIid A : A `&` A = A.
Proof. by apply/msetP=> x; rewrite !msetE minnn. Qed.

Lemma msetIIl A B C : A `&` B `&` C = (A `&` C) `&` (B `&` C).
Proof. by rewrite msetIA !(msetIAC _ C) -(msetIA _ C) msetIid. Qed.

Lemma msetIIr A B C : A `&` (B `&` C) = (A `&` B) `&` (A `&` C).
Proof. by rewrite !(msetIC A) msetIIl. Qed.

(* union *)

Lemma mset0U A : mset0 `|` A = A.
Proof. by apply/msetP => x; rewrite !msetE max0n. Qed.

Lemma msetU0 A : A `|` mset0 = A.
Proof. by rewrite msetUC mset0U. Qed.

Lemma msetUA A B C : A `|` (B `|` C) = A `|` B `|` C.
Proof. by apply/msetP=> x; rewrite !msetE maxnA. Qed.

Lemma msetUCA A B C : A `|` (B `|` C) = B `|` (A `|` C).
Proof. by rewrite !msetUA (msetUC B). Qed.

Lemma msetUAC A B C : A `|` B `|` C = A `|` C `|` B.
Proof. by rewrite -!msetUA (msetUC B). Qed.

Lemma msetUACA A B C D : (A `|` B) `|` (C `|` D) = (A `|` C) `|` (B `|` D).
Proof. by rewrite -!msetUA (msetUCA B). Qed.

Lemma msetUid A : A `|` A = A.
Proof. by apply/msetP=> x; rewrite !msetE maxnn. Qed.

Lemma msetUUl A B C : A `|` B `|` C = (A `|` C) `|` (B `|` C).
Proof. by rewrite msetUA !(msetUAC _ C) -(msetUA _ C) msetUid. Qed.

Lemma msetUUr A B C : A `|` (B `|` C) = (A `|` B) `|` (A `|` C).
Proof. by rewrite !(msetUC A) msetUUl. Qed.

(* adjunction *)

Lemma mset0D A : mset0 `+` A = A.
Proof. by apply/msetP => x; rewrite !msetE add0n. Qed.

Lemma msetD0 A : A `+` mset0 = A.
Proof. by rewrite msetDC mset0D. Qed.

Lemma msetDA A B C : A `+` (B `+` C) = A `+` B `+` C.
Proof. by apply/msetP=> x; rewrite !msetE addnA. Qed.

Lemma msetDCA A B C : A `+` (B `+` C) = B `+` (A `+` C).
Proof. by rewrite !msetDA (msetDC B). Qed.

Lemma msetDAC A B C : A `+` B `+` C = A `+` C `+` B.
Proof. by rewrite -!msetDA (msetDC B). Qed.

Lemma msetDACA A B C D : (A `+` B) `+` (C `+` D) = (A `+` C) `+` (B `+` D).
Proof. by rewrite -!msetDA (msetDCA B). Qed.

(* adjunction, union and difference with one element *)

Lemma msetU1l x A b : x \in A -> x \in A `|` [mset b].
Proof. by move=> Ax; rewrite !inE Ax. Qed.

Lemma msetU1r A b : b \in A `|` [mset b].
Proof. by rewrite !inE eqxx orbT. Qed.

Lemma msetB1P x A b : reflect ((x = b -> A x > 1) /\ x \in A) (x \in A `\ b).
Proof.
rewrite !inE; apply: (iffP andP); first by move=> [/implyP Ax ->]; split => // /eqP.
by move=> [Ax ->]; split => //; apply/implyP => /eqP.
Qed.

Lemma msetB11 b A : (b \in A `\ b) = (A b > 1).
Proof. by rewrite inE eqxx /= in_mset -geq_max. Qed.

Lemma msetB1K a A : a \in A -> a +` (A `\ a) = A.
Proof.
move=> aA; apply/msetP=> x; rewrite !msetE subnKC //=.
by have [->|//] := altP eqP; rewrite mset_gt0.
Qed.

Lemma msetD1K a B : (a +` B) `\ a = B.
Proof. by apply/msetP => x; rewrite !msetE addKn. Qed.

Lemma msetU1K a B : a \notin B -> (a |` B) `\ a = B.
Proof.
move=> aB; apply/msetP=> x; rewrite !msetE.
have [->|] := altP eqP; first by rewrite (mset_eq0P _).
by rewrite max0n subn0.
Qed.

Lemma mset1U1 x B : x \in x |` B. Proof. by rewrite !inE eqxx. Qed.
Lemma mset1D1 x B : x \in x +` B. Proof. by rewrite !inE eqxx. Qed.

Lemma mset1Ur x a B : x \in B -> x \in a |` B.
Proof. by move=> Bx; rewrite !inE predU1r. Qed.
Lemma mset1Dr x a B : x \in B -> x \in a +` B.
Proof. by move=> Bx; rewrite !inE predU1r. Qed.

Lemma mset2P x a b : reflect (x = a \/ x = b) (x \in [mset a; b]).
Proof. by rewrite !inE; apply: (iffP orP) => [] [] /eqP; intuition. Qed.

Lemma in_mset2 x a b : (x \in [mset a; b]) = (x == a) || (x == b).
Proof. by rewrite !inE. Qed.

Lemma mset21 a b : a \in [mset a; b]. Proof. by rewrite mset1D1. Qed.

Lemma mset22 a b : b \in [mset a; b]. Proof. by rewrite in_mset2 eqxx orbT. Qed.

Lemma msetUP x A B : reflect (x \in A \/ x \in B) (x \in A `|` B).
Proof. by rewrite !inE; exact: orP. Qed.

Lemma msetDP x A B : reflect (x \in A \/ x \in B) (x \in A `+` B).
Proof. by rewrite !inE; exact: orP. Qed.

Lemma msetULVR x A B : x \in A `|` B -> (x \in A) + (x \in B).
Proof. by rewrite inE; case: (x \in A); [left|right]. Qed.

Lemma msetDLVR x A B : x \in A `+` B -> (x \in A) + (x \in B).
Proof. by rewrite inE; case: (x \in A); [left|right]. Qed.

(* distribute /cancel *)

Lemma msetIUr A B C : A `&` (B `|` C) = (A `&` B) `|` (A `&` C).
Proof. by apply/msetP=> x; rewrite !msetE minn_maxr. Qed.

Lemma msetIUl A B C : (A `|` B) `&` C = (A `&` C) `|` (B `&` C).
Proof. by apply/msetP=> x; rewrite !msetE minn_maxl. Qed.

Lemma msetUIr A B C : A `|` (B `&` C) = (A `|` B) `&` (A `|` C).
Proof. by apply/msetP=> x; rewrite !msetE maxn_minr. Qed.

Lemma msetUIl A B C : (A `&` B) `|` C = (A `|` C) `&` (B `|` C).
Proof. by apply/msetP=> x; rewrite !msetE maxn_minl. Qed.

Lemma msetUKC A B : (A `|` B) `&` A = A.
Proof. by apply/msetP=> x; rewrite !msetE maxnK. Qed.

Lemma msetUK A B : (B `|` A) `&` A = A.
Proof. by rewrite msetUC msetUKC. Qed.

Lemma msetKUC A B : A `&` (B `|` A) = A.
Proof. by rewrite msetIC msetUK. Qed.

Lemma msetKU A B : A `&` (A `|` B) = A.
Proof. by rewrite msetIC msetUKC. Qed.

Lemma msetIKC A B : (A `&` B) `|` A = A.
Proof. by apply/msetP=> x; rewrite !msetE minnK. Qed.

Lemma msetIK A B : (B `&` A) `|` A = A.
Proof. by rewrite msetIC msetIKC. Qed.

Lemma msetKIC A B : A `|` (B `&` A) = A.
Proof. by rewrite msetUC msetIK. Qed.

Lemma msetKI A B : A `|` (A `&` B) = A.
Proof. by rewrite msetIC msetKIC. Qed.

Lemma msetUKid A B : B `|` A `|` A = B `|` A.
Proof. by rewrite -msetUA msetUid. Qed.

Lemma msetUKidC A B : A `|` B `|` A = A `|` B.
Proof. by rewrite msetUAC msetUid. Qed.

Lemma msetKUid A B : A `|` (A `|` B) = A `|` B.
Proof. by rewrite msetUA msetUid. Qed.

Lemma msetKUidC A B : A `|` (B `|` A) = B `|` A.
Proof. by rewrite msetUCA msetUid. Qed.

Lemma msetIKid A B : B `&` A `&` A = B `&` A.
Proof. by rewrite -msetIA msetIid. Qed.

Lemma msetIKidC A B : A `&` B `&` A = A `&` B.
Proof. by rewrite msetIAC msetIid. Qed.

Lemma msetKIid A B : A `&` (A `&` B) = A `&` B.
Proof. by rewrite msetIA msetIid. Qed.

Lemma msetKIidC A B : A `&` (B `&` A) = B `&` A.
Proof. by rewrite msetICA msetIid. Qed.

Lemma msetDIr A B C : A `+` (B `&` C) = (A `+` B) `&` (A `+` C).
Proof. by apply/msetP=> x; rewrite !msetE addn_minr. Qed.

Lemma msetDIl A B C : (A `&` B) `+` C = (A `+` C) `&` (B `+` C).
Proof. by apply/msetP=> x; rewrite !msetE addn_minl. Qed.

Lemma msetDKIC A B : (A `+` B) `&` A = A.
Proof. by apply/msetP=> x; rewrite !msetE (minn_idPr _) // leq_addr. Qed.

Lemma msetDKI A B : (B `+` A) `&` A = A.
Proof. by rewrite msetDC msetDKIC. Qed.

Lemma msetKDIC A B : A `&` (B `+` A) = A.
Proof. by rewrite msetIC msetDKI. Qed.

Lemma msetKDI A B : A `&` (A `+` B) = A.
Proof. by rewrite msetDC msetKDIC. Qed.

(* adjunction / subtraction *)

Lemma msetDKB A : cancel (msetD A) (msetB^~ A).
Proof. by move=> B; apply/msetP => a; rewrite !msetE addKn. Qed.

Lemma msetDKBC A : cancel (msetD^~ A) (msetB^~ A).
Proof. by move=> B; rewrite msetDC msetDKB. Qed.

Lemma msetBSKl A B a : ((a +` A) `\` B) `\ a = A `\` B.
Proof.
apply/msetP=> b; rewrite !msetE; case: ifPn; rewrite ?add0n ?subn0 //.
by rewrite add1n subn1 subSKn.
Qed.

Lemma msetBDl C A B : (C `+` A) `\` (C `+` B) = A `\` B.
Proof. by apply/msetP=> a; rewrite !msetE subnDl. Qed.

Lemma msetBDr C A B : (A `+` C) `\` (B `+` C) = A `\` B.
Proof. by apply/msetP=> a; rewrite !msetE subnDr. Qed.

Lemma msetBDA A B C : B `\` (A `+` C) = B `\` A `\` C.
Proof. by apply/msetP=> a; rewrite !msetE subnDA. Qed.

Lemma msetUE A B C : msetU A B = A `+` (B `\` A).
Proof. by apply/msetP=> a; rewrite !msetE maxnE. Qed.

(* subset *)

Lemma msubsetP {A B} : reflect (forall x, A x <= B x) (A `<=` B).
Proof.
by apply: (iffP forallP)=> // ? x; case: (in_fsetP A x) => // /mset_eq0P->.
Qed.

Lemma msubset_subset {A B} : A `<=` B -> {subset A <= B}.
Proof.
by move=> /msubsetP AB x; rewrite !in_mset => ?; exact: (leq_trans _ (AB _)).
Qed.

Lemma msetB_eq0 (A B : {mset K}) : (A `\` B == mset0) = (A `<=` B).
Proof.
apply/mset_eqP/msubsetP => AB a;
by have := AB a; rewrite !msetE -subn_eq0 => /eqP.
Qed.

Lemma msubset_refl A : A `<=` A. Proof. exact/msubsetP. Qed.
Hint Resolve msubset_refl.

Lemma msubset_trans : transitive (@msubset K).
Proof.
move=> y x z /msubsetP xy /msubsetP yz ; apply/msubsetP => a.
by apply: (leq_trans (xy _)).
Qed.
Arguments msubset_trans {C A B} _ _ : rename.

Lemma msetUS C A B : A `<=` B -> C `|` A `<=` C `|` B.
Proof.
move=> sAB; apply/msubsetP=> x; rewrite !msetE.
by rewrite geq_max !leq_max leqnn (msubsetP sAB) orbT.
Qed.

Lemma msetDS C A B : A `<=` B -> C `+` A `<=` C `+` B.
Proof.
by move=> /msubsetP sAB; apply/msubsetP=> x; rewrite !msetE leq_add2l.
Qed.

Lemma msetSU C A B : A `<=` B -> A `|` C `<=` B `|` C.
Proof. by move=> sAB; rewrite -!(msetUC C) msetUS. Qed.

Lemma msetSD C A B : A `<=` B -> A `+` C `<=` B `+` C.
Proof. by move=> sAB; rewrite -!(msetDC C) msetDS. Qed.

Lemma msetUSS A B C D : A `<=` C -> B `<=` D -> A `|` B `<=` C `|` D.
Proof. by move=> /(msetSU B) /msubset_trans sAC /(msetUS C)/sAC. Qed.

Lemma msetDSS A B C D : A `<=` C -> B `<=` D -> A `+` B `<=` C `+` D.
Proof. by move=> /(msetSD B) /msubset_trans sAC /(msetDS C)/sAC. Qed.

Lemma msetIidPl {A B} : reflect (A `&` B = A) (A `<=` B).
Proof.
apply: (iffP msubsetP) => [?|<- a]; last by rewrite !msetE geq_min leqnn orbT.
by apply/msetP => a; rewrite !msetE (minn_idPl _).
Qed.

Lemma msetIidPr {A B} : reflect (A `&` B = B) (B `<=` A).
Proof. by rewrite msetIC; apply: msetIidPl. Qed.

Lemma msubsetIidl A B : (A `<=` A `&` B) = (A `<=` B).
Proof.
apply/msubsetP/msubsetP=> sAB a; have := sAB a; rewrite !msetE.
  by rewrite leq_min leqnn.
by move/minn_idPl->.
Qed.

Lemma msubsetIidr A B : (B `<=` A `&` B) = (B `<=` A).
Proof. by rewrite msetIC msubsetIidl. Qed.

Lemma msetUidPr A B : reflect (A `|` B = B) (A `<=` B).
Proof.
apply: (iffP msubsetP) => [AB|<- a]; last by rewrite !msetE leq_max leqnn.
by apply/msetP=> a; rewrite !msetE (maxn_idPr _).
Qed.

Lemma msetUidPl A B : reflect (A `|` B = A) (B `<=` A).
Proof. by rewrite msetUC; apply/msetUidPr. Qed.

Lemma msubsetUl A B : A `<=` A `|` B.
Proof. by apply/msubsetP=> a; rewrite !msetE leq_maxl. Qed.
Hint Resolve msubsetUl.

Lemma msubsetUr A B : B `<=` (A `|` B).
Proof. by rewrite msetUC. Qed.
Hint Resolve msubsetUr.

Lemma msubsetU1 x A : A `<=` (x |` A).
Proof. by rewrite msubsetUr. Qed.
Hint Resolve msubsetU1.

Lemma msubsetU A B C : (A `<=` B) || (A `<=` C) -> A `<=` (B `|` C).
Proof. by move=> /orP [] /msubset_trans ->. Qed.

Lemma eqEmsubset A B : (A == B) = (A `<=` B) && (B `<=` A).
Proof.
apply/eqP/andP => [<-|[/msubsetP AB /msubsetP BA]]; first by split.
by apply/msetP=> a; apply/eqP; rewrite eqn_leq AB BA.
Qed.

Lemma subEmproper A B : A `<=` B = (A == B) || (A `<` B).
Proof. by rewrite eqEmsubset -andb_orr orbN andbT. Qed.

Lemma mproper_sub A B : A `<` B -> A `<=` B.
Proof. by rewrite subEmproper orbC => ->. Qed.

Lemma eqVmproper A B : A `<=` B -> A = B \/ A `<` B.
Proof. by rewrite subEmproper => /predU1P. Qed.

Lemma mproperEneq A B : A `<` B = (A != B) && (A `<=` B).
Proof. by rewrite andbC eqEmsubset negb_and andb_orr andbN. Qed.

Lemma mproper_neq A B : A `<` B -> A != B.
Proof. by rewrite mproperEneq; case/andP. Qed.

Lemma eqEmproper A B : (A == B) = (A `<=` B) && ~~ (A `<` B).
Proof. by rewrite negb_and negbK andb_orr andbN eqEmsubset. Qed.

(* Lemma eqEfcard A B : (A == B) = (A `<=` B) && (#|` B| <= #|` A|)%N. *)
(* Proof. *)
(* rewrite -(inj_in_eq (@msub_inj (A `|` B))) -?topredE //=. *)
(* by rewrite eqEcard !(@subset_msubE (A `|` B)) ?(@card_msub (A `|` B)). *)
(* Qed. *)

(* Lemma mproperEcard A B : *)
(*   (A `<` B) = (A `<=` B) && (#|` A| < #|` B|)%N. *)
(* Proof. by rewrite mproperEneq ltnNge andbC eqEfcard; case: (A `<=` B). Qed. *)

(* Lemma msubset_leqif_cards A B : A `<=` B -> (#|` A| <= #|` B| ?= iff (A == B))%N. *)
(* Proof. *)
(* rewrite -!(@card_msub (A `|` B)) // -(@subset_msubE (A `|` B)) //. *)
(* by move=> /subset_leqif_cards; rewrite (inj_in_eq (@msub_inj _)) -?topredE /=. *)
(* Qed. *)

Lemma msub0set A : msubset mset0 A.
Proof. by apply/msubsetP=> x; rewrite msetE. Qed.
Hint Resolve msub0set.

Lemma msubset0 A : (A `<=` mset0) = (A == mset0).
Proof. by rewrite eqEmsubset msub0set andbT. Qed.

Lemma mproper0 A : (mproper mset0 A) = (A != mset0).
Proof. by rewrite /mproper msub0set msubset0. Qed.

Lemma mproperE A B : (A `<` B) = (A `<=` B) && ~~ (msubset B A).
Proof. by []. Qed.

Lemma msubEproper A B : (A `<=` B) = (A == B) || (A `<` B).
Proof. by rewrite mproperEneq; case: eqP => //= ->; apply: msubset_refl. Qed.

(* Lemma msubset_leq_card A B : A `<=` B -> (#|` A| <= #|` B|)%N. *)
(* Proof. by move=> /msubset_leqif_cards ->. Qed. *)

(* Lemma mproper_ltn_card A B : A `<` B -> (#|` A| < #|` B|)%N. *)
(* Proof. by rewrite mproperEcard => /andP []. Qed. *)

(* Lemma msubset_cardP A B : #|` A| = #|` B| -> *)
(*   reflect (A =i B) (A `<=` B). *)
(* Proof. *)
(* move=> eq_cardAB; apply: (iffP idP) => [/eqVmproper [->//|]|/msetP -> //]. *)
(* by rewrite mproperEcard eq_cardAB ltnn andbF. *)
(* Qed. *)

Lemma mproper_sub_trans B A C : A `<` B -> msubset B C -> A `<` C.
Proof.
move=> /andP [NAB AB] BC; rewrite /mproper.
Admitted.

(* Lemma msub_proper_trans B A C : *)
(*   A `<=` B -> B `<` C -> A `<` C. *)
(* Proof. *)
(* rewrite !mproperEcard => sAB /andP [sBC lt_BC]. *)
(* by rewrite (msubset_trans sAB) //= (leq_ltn_trans _ lt_BC) // msubset_leq_card. *)
(* Qed. *)

Lemma msubset_neq0 A B : A `<=` B -> A != mset0 -> B != mset0.
Proof. by rewrite -!mproper0 => sAB /mproper_sub_trans->. Qed.

(* msub is a morphism *)

Lemma msetBDKC A B : A `<=` B -> A `+` (B `\` A) = B.
Proof. by move=> /msubsetP AB; apply/msetP=> a; rewrite !msetE subnKC. Qed.

Lemma msetBDK A B : A `<=` B -> B `\` A `+` A = B.
Proof. by move=> /msubsetP AB; apply/msetP => a; rewrite !msetE subnK. Qed.

Lemma msetBBK A B : A `<=` B -> B `\` (B `\` A) = A.
Proof. by move=> /msubsetP AB; apply/msetP => a; rewrite !msetE subKn. Qed.

Lemma msetBD1K A B a : A `<=` B -> A a < B a -> a +` (B `\` (a +` A)) = B `\` A.
Proof.
move=> /msubsetP AB ABa; apply/msetP => b; rewrite !msetE.
by case: ifP => //= /eqP->; rewrite !add1n subnSK.
Qed.

Lemma subset_msetBLR A B C : (msubset (A `\` B) C) = (A `<=` B `+` C).
Proof.
apply/msubsetP/msubsetP => [] sABC a;
by have := sABC a; rewrite !msetE ?leq_subLR.
Qed.

Lemma mproperP {A B} : reflect (forall x, A x < B x) (A `<` B).
Proof. Admitted.

Lemma proper_msetBRL A B C : (B `<` (C `\` A)) = ((A `+` B) `<` C).
Proof.
apply/mproperP/mproperP => [] sABC a;
by have := sABC a; rewrite !msetE ?ltn_subRL.
Qed.

Lemma msetnP n x a : reflect (0 < n /\ x = a) (x \in msetn n a).
Proof. by do [apply: (iffP idP); rewrite !inE] => [/andP[]|[]] -> /eqP. Qed.

Lemma gt0_msetnP n x a : 0 < n -> reflect (x = a) (x \in msetn n a).
Proof. by move=> n_gt0; rewrite inE n_gt0 /=; exact: eqP. Qed.

Lemma msetn1 n a : a \in msetn n a = (n > 0).
Proof. by rewrite inE eqxx andbT. Qed.

Lemma mset1P x a : reflect (x = a) (x \in [mset a]).
Proof. by rewrite inE; exact: eqP. Qed.

Lemma mset11 a : a \in [mset a]. Proof. by rewrite inE /=. Qed.

Lemma msetn_inj n : n > 0 -> injective (@msetn K n).
Proof.
move=> n_gt0 a b eqsab; apply/(gt0_msetnP _ _ _ n_gt0).
by rewrite -eqsab inE n_gt0 eqxx.
Qed.

Lemma mset1UP x a B : reflect (x = a \/ x \in B) (x \in a |` B).
Proof. by rewrite !inE; exact: predU1P. Qed.

Lemma mset_cons a s : seq_mset (a :: s) = a +` (seq_mset s).
Proof. by apply/msetP=> x; rewrite !msetE /= eq_sym. Qed.

(* We need separate lemmas for the explicit enumerations since they *)
(* associate on the left.   *)

(* intersection *)

Lemma msetIP x A B : reflect (x \in A /\ x \in B) (x \in A `&` B).
Proof. by rewrite inE; apply: andP. Qed.

Lemma msetIS C A B : A `<=` B -> C `&` A `<=` C `&` B.
Proof.
move=> sAB; apply/msubsetP=> x; rewrite !msetE.
by rewrite leq_min !geq_min leqnn (msubsetP sAB) orbT.
Qed.

Lemma msetSI C A B : A `<=` B -> A `&` C `<=` B `&` C.
Proof. by move=> sAB; rewrite -!(msetIC C) msetIS. Qed.

Lemma msetISS A B C D : A `<=` C -> B `<=` D -> A `&` B `<=` C `&` D.
Proof. by move=> /(msetSI B) /msubset_trans sAC /(msetIS C) /sAC. Qed.

(* difference *)

(* Lemma msetBP A B x : reflect (x \in A /\ x \notin B) (x \in A `\` B). *)

Lemma msetSB C A B : A `<=` B -> A `\` C `<=` B `\` C.
Proof.
by move=> /msubsetP sAB; apply/msubsetP=> x; rewrite !msetE leq_sub2r.
Qed.

Lemma msetBS C A B : A `<=` B -> C `\` B `<=` C `\` A.
Proof.
by move=> /msubsetP sAB; apply/msubsetP=> x; rewrite !msetE leq_sub2l.
Qed.

Lemma msetBSS A B C D : A `<=` C -> D `<=` B -> A `\` B `<=` C `\` D.
Proof. by move=> /(msetSB B) /msubset_trans sAC /(msetBS C) /sAC. Qed.

Lemma msetB0 A : A `\` mset0 = A.
Proof. by apply/msetP=> x; rewrite !msetE subn0. Qed.

Lemma mset0B A : mset0 `\` A = mset0.
Proof. by apply/msetP=> x; rewrite !msetE sub0n. Qed.

Lemma msetBxx A : A `\` A = mset0.
Proof. by apply/msetP=> x; rewrite !msetE subnn. Qed.

(* Lemma msetIB A B : A `&` B `+` A `\` B = A. *)
(* Proof. apply/msetP => a; rewrite !msetE. *)

(* Lemma msetDUl A B C : (A `|` B) `\` C = (A `\` C) `|` (B `\` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetDUr A B C : A `\` (B `|` C) = (A `\` B) `&` (A `\` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetDIl A B C : (A `&` B) `\` C = (A `\` C) `&` (B `\` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetIDA A B C : A `&` (B `\` C) = (A `&` B) `\` C. *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetIDAC A B C : (A `\` B) `&` C = (A `&` C) `\` B. *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetDIr A B C : A `\` (B `&` C) = (A `\` B) `|` (A `\` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetDDl A B C : (A `\` B) `\` C = A `\` (B `|` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetDDr A B C : A `\` (B `\` C) = (A `\` B) `|` (A `&` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetUDl (A B C : {mset K}) : A `|` (B `\` C) = (A `|` B) `\` (C `\` A). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* Lemma msetUDr (A B C : {mset K}) : (A `\` B) `|` C = (A `|` C) `\` (B `\` C). *)
(* Proof. by apply/msetP=> x; rewrite !inE; do ?case: (_ \in _). Qed. *)

(* other inclusions *)

Lemma msubsetIl A B : A `&` B `<=` A.
Proof. by apply/msubsetP=> x; rewrite msetE geq_minl. Qed.

Lemma msubsetIr A B : A `&` B `<=` B.
Proof. by apply/msubsetP=> x; rewrite msetE geq_minr. Qed.

Lemma msubsetDl A B : A `\` B `<=` A.
Proof. by apply/msubsetP=> x; rewrite msetE leq_subLR leq_addl. Qed.

Lemma msubD1set A x : A `\ x `<=` A.
Proof. by rewrite msubsetDl. Qed.

Hint Resolve msubsetIl msubsetIr msubsetDl msubD1set.

(* cardinal lemmas for msets *)

(* Lemma cardfs0 : #|` @mset0 K| = 0. *)
(* Proof. by rewrite -(@card_msub mset0) // msub0 cards0. Qed. *)

(* Lemma cardfs_eq0 A : (#|` A| == 0) = (A == mset0). *)
(* Proof. by rewrite -(@card_msub A) // cards_eq0 msub_eq0. Qed. *)

(* Lemma cardfs0_eq A : #|` A| = 0 -> A = mset0. *)
(* Proof. by move=> /eqP; rewrite cardfs_eq0 => /eqP. Qed. *)

(* Lemma mset0Pn A : reflect (exists x, x \in A) (A != mset0). *)
(* Proof. *)
(* rewrite -cardfs_eq0; apply: (equivP existsP). *)
(* by split=> [] [a aP]; [exists (val a); apply: valP|exists (MsetSub aP)]. *)
(* Qed. *)

(* Lemma cardfs_gt0 A : (0 < #|` A|)%N = (A != mset0). *)
(* Proof. by rewrite lt0n cardfs_eq0. Qed. *)

(* Lemma cardfsE s : #|` seq_mset s| = size (undup s). *)
(* Proof. *)
(* rewrite cardT enumT unlock /= undup_id ?pmap_sub_uniq ?[seq_mset]unlock //=. *)
(* by rewrite size_pmap_sub (@eq_in_count _ _ predT) ?count_predT ?size_sort_keys. *)
(* Qed. *)

(* Lemma cardfs1 x : #|` [mset x]| = 1. *)
(* Proof. by rewrite cardfsE undup_id. Qed. *)

(* Lemma cardfsUI A B : #|` A `|` B| + #|` A `&` B| = #|` A| + #|` B|. *)
(* Proof. *)
(* rewrite -!(@card_msub (A `|` B)) ?(msubset_trans (msubsetIl _ _)) //. *)
(* by rewrite msubU msubI cardsUI. *)
(* Qed. *)

(* Lemma cardfsU A B : #|` A `|` B| = (#|` A| + #|` B| - #|` A `&` B|)%N. *)
(* Proof. by rewrite -cardfsUI addnK. Qed. *)

(* Lemma cardfsI A B : #|` A `&` B| = (#|` A| + #|` B| - #|` A `|` B|)%N. *)
(* Proof. by rewrite  -cardfsUI addKn. Qed. *)

(* Lemma cardfsID B A : #|` A `&` B| + #|` A `\` B| = #|` A|. *)
(* Proof. by rewrite -!(@card_msub A) // msubI msubD cardsID. Qed. *)

(* Lemma cardfsD A B : #|` A `\` B| = (#|` A| - #|` A `&` B|)%N. *)
(* Proof. by rewrite -(cardfsID B A) addKn. Qed. *)

Lemma mem_mset1U a A : a \in A -> a |` A = A.
Proof.
rewrite in_mset => aA; apply/msetP => x; rewrite !msetE (maxn_idPr _) //.
by have [->|//] := altP eqP; rewrite (leq_trans _ aA).
Qed.

Lemma mem_msetD1 a A : a \notin A -> A `\ a = A.
Proof.
move=> /mset_eq0P aA; apply/msetP => x; rewrite !msetE.
by have [->|] := altP eqP; rewrite ?aA ?subn0.
Qed.

Lemma msetIn a A n : A `&` msetn n a = msetn (minn (A a) n) a.
Proof.
by apply/msetP => x; rewrite !msetE; have [->|] := altP eqP; rewrite ?minn0.
Qed.

(* Lemma cardfsU1 a A : #|` a |` A| = (a \notin A) + #|` A|. *)
(* Proof. *)
(* have [aA|aNA] := boolP (a \in A); first by rewrite mem_mset1U. *)
(* rewrite cardfsU -addnBA ?msubset_leq_card // msetIC -cardfsD. *)
(* by rewrite mem_msetD1 // cardfs1. *)
(* Qed. *)

(* Lemma cardfs2 a b : #|` [mset a; b]| = (a != b).+1. *)
(* Proof. by rewrite !cardfsU1 cardfs1 addn1 seq_msetE in_cons orbF. Qed. *)

(* Lemma cardfsD1 a A : #|` A| = (a \in A) + #|` A `\ a|. *)
(* Proof. *)
(* rewrite -(cardfsID [mset a]) msetI1 (fun_if (fun A => #|` A|)). *)
(* by rewrite cardfs0 cardfs1; case: (_ \in _). *)
(* Qed. *)

(* other inclusions *)

(* Lemma msub1set A x : ([mset x] `<=` A) = (x \in A). *)
(* Proof. *)
(* rewrite -(@subset_msubE (x |` A)) // msub1 ?mset1U1 // => xxA. *)
(* by rewrite sub1set inE. *)
(* Qed. *)

(* Lemma cardfs1P A : reflect (exists x, A = [mset x]) (#|` A| == 1). *)
(* Proof. *)
(* apply: (iffP idP) => [|[x ->]]; last by rewrite cardfs1. *)
(* rewrite eq_sym eqn_leq cardfs_gt0=> /andP[/mset0Pn[x Ax] leA1]. *)
(* by exists x; apply/eqP; rewrite eq_sym eqEfcard msub1set cardfs1 leA1 Ax. *)
(* Qed. *)

(* Lemma msubset1 A x : (A `<=` [mset x]) = (A == [mset x]) || (A == mset0). *)
(* Proof. *)
(* rewrite eqEfcard cardfs1 -cardfs_eq0 orbC andbC. *)
(* by case: posnP => // A0; rewrite (cardfs0_eq A0) msub0set. *)
(* Qed. *)

(* Implicit Arguments msetIidPl [A B]. *)

(* Lemma cardfsDS A B : B `<=` A -> #|` A `\` B| = (#|` A| - #|` B|)%N. *)
(* Proof. by rewrite cardfsD => /msetIidPr->. Qed. *)

Lemma msubIset A B C : (B `<=` A) || (C `<=` A) -> (B `&` C `<=` A).
Proof. by case/orP; apply: msubset_trans; rewrite (msubsetIl, msubsetIr). Qed.

Lemma msubsetI A B C : (A `<=` B `&` C) = (A `<=` B) && (A `<=` C).
Proof.
rewrite !(sameP msetIidPl eqP) msetIA; have [-> //| ] := altP (A `&` B =P A).
by apply: contraNF => /eqP <-; rewrite -msetIA -msetIIl msetIAC.
Qed.

Lemma msubsetIP A B C : reflect (A `<=` B /\ A `<=` C) (A `<=` B `&` C).
Proof. by rewrite msubsetI; exact: andP. Qed.

Lemma msubUset A B C : (B `|` C `<=` A) = (B `<=` A) && (C `<=` A).
Proof.
apply/idP/idP => [subA|/andP [AB CA]]; last by rewrite -[A]msetUid msetUSS.
by rewrite !(msubset_trans _ subA).
Qed.

Lemma msubUsetP A B C : reflect (A `<=` C /\ B `<=` C) (A `|` B `<=` C).
Proof. by rewrite msubUset; exact: andP. Qed.

Lemma msetU_eq0 A B : (A `|` B == mset0) = (A == mset0) && (B == mset0).
Proof. by rewrite -!msubset0 msubUset. Qed.

Lemma setD_eq0 A B : (A `\` B == mset0) = (A `<=` B).
Proof. by rewrite -msubset0 subset_msetBLR msetD0. Qed.

(* Lemma msubsetD1 A B x : (A `<=` B `\ x) = (A `<=` B) && (x \notin A). *)
(* Proof. *)
(* do !rewrite -(@subset_msubE (x |` A `|` B)) ?msubDset ?msetUA // 1?msetUAC //. *)
(* rewrite msubD1 => [|mem_x]; first by rewrite -msetUA mset1U1. *)
(* by rewrite subsetD1 // inE. *)
(* Qed. *)

(* Lemma msubsetD1P A B x : reflect (A `<=` B /\ x \notin A) (A `<=` B `\ x). *)
(* Proof. by rewrite msubsetD1; exact: andP. Qed. *)

(* Lemma msubsetPn A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A `<=` B)). *)
(* Proof. *)
(*  rewrite -msetD_eq0; apply: (iffP (mset0Pn _)) => [[x]|[x xA xNB]]. *)
(*   by rewrite inE => /andP[]; exists x. *)
(* by exists x; rewrite inE xA xNB. *)
(* Qed. *)

(* Lemma mproperD1 A x : x \in A -> A `\ x `<` A. *)
(* Proof. *)
(* move=> Ax; rewrite mproperE msubsetDl; apply/msubsetPn; exists x=> //. *)
(* by rewrite in_msetD1 Ax eqxx. *)
(* Qed. *)

(* Lemma mproperIr A B : ~~ (B `<=` A) -> A `&` B `<` B. *)
(* Proof. by move=> nsAB; rewrite mproperE msubsetIr msubsetI negb_and nsAB. Qed. *)

(* Lemma mproperIl A B : ~~ (A `<=` B) -> A `&` B `<` A. *)
(* Proof. by move=> nsBA; rewrite mproperE msubsetIl msubsetI negb_and nsBA orbT. Qed. *)

(* Lemma mproperUr A B : ~~ (A `<=` B) ->  B `<` A `|` B. *)
(* Proof. by rewrite mproperE msubsetUr msubUset msubset_refl /= andbT. Qed. *)

(* Lemma mproperUl A B : ~~ (B `<=` A) ->  A `<` A `|` B. *)
(* Proof. by move=> not_sBA; rewrite msetUC mproperUr. Qed. *)

(* Lemma mproper1set A x : ([mset x] `<` A) -> (x \in A). *)
(* Proof. by move/mproper_sub; rewrite msub1set. Qed. *)

(* Lemma mproperIset A B C : (B `<` A) || (C `<` A) -> (B `&` C `<` A). *)
(* Proof. by case/orP; apply: msub_proper_trans; rewrite (msubsetIl, msubsetIr). Qed. *)

(* Lemma mproperI A B C : (A `<` B `&` C) -> (A `<` B) && (A `<` C). *)
(* Proof. *)
(* move=> pAI; apply/andP. *)
(* by split; apply: (mproper_sub_trans pAI); rewrite (msubsetIl, msubsetIr). *)
(* Qed. *)

(* Lemma mproperU A B C : (B `|` C `<` A) -> (B `<` A) && (C `<` A). *)
(* Proof. *)
(* move=> pUA; apply/andP. *)
(* by split; apply: msub_proper_trans pUA; rewrite (msubsetUr, msubsetUl). *)
(* Qed. *)

(* Lemma msetI_eq0 A B : (A `&` B == mset0) = [disjoint A & B]. *)
(* Proof. by []. Qed. *)

(* Lemma fdisjoint_sub {A B} : [disjoint A & B]%mset -> *)
(*   forall C : {mset K}, [disjoint msub C A & msub C B]%bool. *)
(* Proof. *)
(* move=> disjointAB C; apply/pred0P => a /=; rewrite !inE. *)
(* by have /eqP /msetP /(_ (val a)) := disjointAB; rewrite !inE. *)
(* Qed. *)

(* Lemma disjoint_msub C A B : A `|` B `<=` C -> *)
(*   [disjoint msub C A & msub C B]%bool = [disjoint A & B]. *)
(* Proof. *)
(* move=> ABsubC. *)
(* apply/idP/idP=> [/pred0P DAB|/fdisjoint_sub->//]; apply/eqP/msetP=> a. *)
(* rewrite !inE; have [aC|] := boolP (a \in A `|` B); last first. *)
(*   by rewrite !inE => /norP [/negPf-> /negPf->]. *)
(* by have /= := DAB (MsetSub (msubsetP ABsubC _ aC)); rewrite !inE. *)
(* Qed. *)

(* Lemma fdisjointP {A B} : *)
(*   reflect (forall a, a \in A -> a \notin B) [disjoint A & B]%mset. *)
(* Proof. *)
(* apply: (iffP eqP) => [AIB_eq0 a aA|neq_ab]. *)
(*   by have /msetP /(_ a) := AIB_eq0; rewrite !inE aA /= => ->. *)
(* apply/msetP => a; rewrite !inE. *)
(* by case: (boolP (a \in A)) => // /neq_ab /negPf ->. *)
(* Qed. *)

(* Lemma msetDidPl A B : reflect (A `\` B = A) [disjoint A & B]%mset. *)
(* Proof. *)
(* apply: (iffP fdisjointP)=> [NB|<- a]; last by rewrite inE => /andP[]. *)
(* apply/msetP => a; rewrite !inE andbC. *)
(* by case: (boolP (a \in A)) => //= /NB ->. *)
(* Qed. *)

(* Lemma disjoint_msetI0 A B : [disjoint A & B] -> A `&` B = mset0. *)
(* Proof. by rewrite -msetI_eq0; move/eqP. Qed. *)

(* Lemma msubsetD A B C : *)
(*   (A `<=` (B `\` C)) = (A `<=` B) && [disjoint A & C]%mset. *)
(* Proof. *)
(* pose D := A `|` B `|` C. *)
(* have AD : A `<=` D by rewrite /D -msetUA msubsetUl. *)
(* have BD : B `<=` D by rewrite /D msetUAC msubsetUr. *)
(* rewrite -(@subset_msubE D) //; last first. *)
(*   by rewrite msubDset (msubset_trans BD) // msubsetUr. *)
(* rewrite msubD subsetD !subset_msubE // disjoint_msub //. *)
(* by rewrite /D msetUAC msubsetUl. *)
(* Qed. *)

(* Lemma msubsetDP A B C : *)
(*    reflect (A `<=` B /\ [disjoint A & C]%mset) (A `<=` (B `\` C)). *)
(* Proof. by rewrite msubsetD; apply: andP. Qed. *)

(* Lemma fdisjoint_sym A B : [disjoint A & B] = [disjoint B & A]. *)
(* Proof. by rewrite -!msetI_eq0 msetIC. Qed. *)

(* Lemma fdisjointP_sym {A B} : *)
(*   reflect (forall a, a \in A -> a \notin B) [disjoint B & A]%mset. *)
(* Proof. by rewrite fdisjoint_sym; apply: fdisjointP. Qed. *)

(* Lemma fdisjoint_trans A B C : *)
(*    A `<=` B -> [disjoint B & C] -> [disjoint A & C]. *)
(* Proof. *)
(* move=> AsubB; rewrite -!(@disjoint_msub (B `|` C)) ?msetSU //. *)
(* by apply: disjoint_trans; rewrite subset_msub. *)
(* Qed. *)

(* Lemma fdisjoint0X A : [disjoint mset0 & A]. *)
(* Proof. by rewrite -msetI_eq0 mset0I. Qed. *)

(* Lemma fdisjointX0 A : [disjoint A & mset0]. *)
(* Proof. by rewrite -msetI_eq0 msetI0. Qed. *)

(* Lemma fdisjoint1X x A : [disjoint [mset x] & A] = (x \notin A). *)
(* Proof. *)
(* rewrite -(@disjoint_msub (x |` A)) //. *)
(* by rewrite (@eq_disjoint1 _ (MsetSub (mset1U1 _ _))) ?inE =>// ?; rewrite !inE. *)
(* Qed. *)

(* Lemma fdisjointX1 x A : [disjoint A & [mset x]] = (x \notin A). *)
(* Proof. by rewrite fdisjoint_sym fdisjoint1X. Qed. *)

(* Lemma fdisjointUX A B C : *)
(*    [disjoint A `|` B & C] = [disjoint A & C]%mset && [disjoint B & C]%mset. *)
(* Proof. by rewrite -!msetI_eq0 msetIUl msetU_eq0. Qed. *)

(* Lemma fdisjointXU A B C : *)
(*    [disjoint A & B `|` C] = [disjoint A & B]%mset && [disjoint A & C]%mset. *)
(* Proof. by rewrite -!msetI_eq0 msetIUr msetU_eq0. Qed. *)

(* Lemma fdisjointU1X x A B : *)
(*    [disjoint x |` A & B]%mset = (x \notin B) && [disjoint A & B]%mset. *)
(* Proof. by rewrite fdisjointUX fdisjoint1X. Qed. *)

End MSetTheory.

author: strub

repo: glv

save_path: github-repos/coq/strub-glv


text:
Require Import GeoCoq.Tarski_dev.Ch09_plane.
Require Import NArith.
Require Import GeoCoq.Utils.sets.
Require Import GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_cop.
Require Import GeoCoq.Tactics.Coinc.CoincR.

Section CoincR_for_cop.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition ss_ok_for_cop ss interp :=
  @ss_ok Tarski_is_a_Arity_for_cop
         Tarski_is_a_Coinc_predicates_for_cop ss interp.

Lemma ss_ok_empty_for_cop : forall interp, ss_ok_for_cop SS.empty interp.
Proof. exact ss_ok_empty. Qed.

Lemma collect_coincs_for_cop : forall A B C D pa pb pc pd ss interp,
  Coplanar A B C D ->
  interp pa = A ->
  interp pb = B ->
  interp pc = C ->
  interp pd = D ->
  ss_ok_for_cop ss interp ->
  ss_ok_for_cop (SS.add (@CPToSS 4 (pa, (pb, (pc, pd)))) ss) interp.
Proof.
intros A B C D pa pb pc pd ss interp HCop HA HB HC HD HSS.
apply (@collect_coincs Tarski_is_a_Arity_for_cop
                       Tarski_is_a_Coinc_predicates_for_cop);
[apply Tarski_is_a_Coinc_theory_for_cop|simpl|auto].
rewrite HA; rewrite HB; rewrite HC; rewrite HD; auto.
Qed.

Definition st_ok_for_cop st interp :=
  @st_ok Tarski_is_a_Arity_for_cop
         Tarski_is_a_Coinc_predicates_for_cop st interp.

Lemma st_ok_empty_for_cop : forall interp, st_ok_for_cop STempty interp.
Proof. exact st_ok_empty. Qed.

Lemma collect_wds_for_cop : forall A B C pa pb pc st interp,
  ~ Col A B C ->
  interp pa = A ->
  interp pb = B ->
  interp pc = C ->
  st_ok_for_cop st interp ->
  st_ok_for_cop (STadd (pa, (pb, pc)) st) interp.
Proof.
intros A B C pa pb pc st interp HDiff HA HB HC HST.
apply (@collect_wds Tarski_is_a_Arity_for_cop
                    Tarski_is_a_Coinc_predicates_for_cop);
[apply Tarski_is_a_Coinc_theory_for_cop|simpl|auto].
rewrite HA; rewrite HB; rewrite HC; auto.
Qed.

Definition test_coinc_for_cop ss st (pa pb pc pd : positive) :=
  @test_coinc Tarski_is_a_Arity_for_cop ss st (pa, (pb, (pc, pd))).

Definition interp_CP_for_cop (pa pb pc pd : positive) interp :=
  @interp_CP Tarski_is_a_Arity_for_cop 3 (pa, (pb, (pc, pd))) interp.

Lemma test_coinc_ok_for_cop : forall pa pb pc pd ss st interp,
  ss_ok_for_cop ss interp ->
  st_ok_for_cop st interp ->
  test_coinc_for_cop ss st pa pb pc pd = true ->
  Coplanar (interp pa) (interp pb) (interp pc) (interp pd).
Proof.
intros pa pb pc pd ss st interp HSS HST HTest.
assert (HCop := @test_coinc_ok Tarski_is_a_Arity_for_cop
                               Tarski_is_a_Coinc_predicates_for_cop
                               Tarski_is_a_Coinc_theory_for_cop
                               ss st interp (pa, (pb, (pc, pd))) HSS HST HTest).
simpl in HCop; auto.
Qed.

End CoincR_for_cop.

Ltac assert_ss_ok Tpoint Cop lvar :=
  repeat
  match goal with
    | HCop : Cop ?A ?B ?C ?D, HOK : ss_ok_for_cop ?SS ?Interp |- _ =>
      let pa := List_assoc Tpoint A lvar in
      let pb := List_assoc Tpoint B lvar in
      let pc := List_assoc Tpoint C lvar in
      let pd := List_assoc Tpoint D lvar in
      apply PropToTagged in HCop;
      apply (collect_coincs_for_cop A B C D pa pb pc pd SS Interp HCop) in HOK;
      try reflexivity
  end.

Ltac assert_st_ok Tpoint Col lvar :=
  repeat
  match goal with
    | HNCol : ~ Col ?A ?B ?C, HOK : st_ok_for_cop ?ST ?Interp |- _ =>
      let pa := List_assoc Tpoint A lvar in
      let pb := List_assoc Tpoint B lvar in
      let pc := List_assoc Tpoint C lvar in
      apply PropToTagged in HNCol;
      apply (collect_wds_for_cop A B C pa pb pc ST Interp HNCol) in HOK;
      try reflexivity
  end.

Ltac Cop_refl Tpoint Col Cop :=
  match goal with
    | Default : Tpoint |- Cop ?A ?B ?C ?D =>
      let lvar := build_numbered_points_list Tpoint in
      let pa := List_assoc Tpoint A lvar in
      let pb := List_assoc Tpoint B lvar in
      let pc := List_assoc Tpoint C lvar in
      let pd := List_assoc Tpoint D lvar in
      let c := ((vm_compute;reflexivity) || fail 2 "Can not be deduced") in
      let HSS := fresh in
      assert (HSS := ss_ok_empty_for_cop (interp lvar Default));
      assert_ss_ok Tpoint Cop lvar;
      let HST := fresh in
      assert (HST := st_ok_empty_for_cop (interp lvar Default));
      assert_st_ok Tpoint Col lvar;
      match goal with
        | HOKSS : ss_ok_for_cop ?SS ?Interp, HOKST : st_ok_for_cop ?ST ?Interp |- _ =>
          apply (test_coinc_ok_for_cop pa pb pc pd SS ST
                                       Interp HOKSS HOKST); c
      end
  end.
(*
Section Test.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Goal forall P24 P23 P22 P21 P20 P19 P18 P17 P16 P15 P14 P13 P12 P11 P10 P9 P8 P7 P6 P5 P4 P3 P2 P1 P0,
  Coplanar P1 P0 P2 P12 -> Coplanar P8 P2 P0 P1 -> ~ Col P18 P20 P19 ->
  Coplanar P19 P2 P1 P0 -> Coplanar P1 P15 P2 P0 -> Coplanar P23 P13 P12 P14 ->
  ~ Col P10 P9 P11 -> Coplanar P1 P2 P18 P0 -> Coplanar P11 P2 P1 P0 ->
  ~ Col P2 P1 P0 -> Coplanar P0 P1 P2 P6 -> Coplanar P16 P2 P1 P0 ->
  Coplanar P15 P22 P16 P17 -> Coplanar P2 P1 P0 P17 -> Coplanar P20 P0 P2 P1 ->
  Coplanar P1 P2 P0 P4 -> Coplanar P13 P1 P2 P0 -> ~ Col P7 P8 P6 ->
  Coplanar P2 P9 P1 P0 -> Coplanar P2 P10 P0 P1 -> Coplanar P1 P0 P14 P2 ->
  Coplanar P1 P7 P0 P2 -> ~ Col P4 P5 P3 -> Coplanar P0 P3 P1 P2 ->
  Coplanar P24 P11 P9 P10 -> ~ Col P14 P13 P12 -> ~ Col P15 P17 P16 ->
  Coplanar P18 P21 P20 P19 -> Coplanar P0 P5 P2 P1 ->
  Coplanar P21 P22 P23 P24.
Proof.
intros.
Time Cop_refl Tpoint Col Coplanar.
Qed.

End Test.
*)

author: GeoCoq

repo: GeoCoq

save_path: github-repos/coq/GeoCoq-GeoCoq


text:
From Equations Require Import Equations.
Require Import Coq.Lists.List.
Require Import Coq.Arith.PeanoNat.

Require Export SystemFR.ReducibilityEquivalent.
Require Export SystemFR.ErasedArrow.
Require Export SystemFR.ErasedPair.
Require Export SystemFR.ErasedQuant.
Require Export SystemFR.ErasedNat.
Require Export SystemFR.ErasedPrimitive.

Require Import Psatz.

Opaque reducible_values.
Opaque makeFresh.

Lemma reducible_fix_zero:
  forall ρ T ts v,
    wf ts 1 ->
    wf T 1 ->
    pfv ts term_var = nil ->
    pfv T term_var = nil ->
    valid_interpretation ρ ->
    is_erased_term ts ->
    is_erased_type T ->
    notype_tfix ts ~>* v ->
    cbv_value v ->
    (forall tx n,
      [ ρ ⊨ n : T_nat ]v ->
      [ ρ ⊨ tx : T_forall (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) n)) T ]v ->
      [ tx ≡ notype_tfix ts ] ->
      [ ρ ⊨ open 0 ts tx : open 0 T n ]) ->
    [ ρ ⊨ notype_tfix ts : open 0 T zero ].
Proof.
  intros.
  eapply backstep_reducible; steps;
    eauto with smallstep;
    eauto with wf.

  apply reducibility_equivalent2 with (open 0 (open 1 ts zero) v);
    repeat step || apply equivalent_context || simp_red_goal || simp_red_top_level_hyp ||
           apply_any ||
           rewrite (open_none ts) by (steps; unshelve eauto with wf; auto);
    try solve [ apply equivalent_sym; equivalent_star ];
    try solve [ last_step_binary_primitive ];
    eauto 2 with wf fv erased step_tactic.

  unfold closed_value, closed_term; steps;
    eauto using wf_star_smallstep with fv wf erased step_tactic.
Qed.

Lemma scbv_step_fix_open:
  forall ts,
    wf ts 1 ->
    notype_tfix ts ~> open 0 ts (notype_tfix ts).
Proof.
  intros.
  eapply scbv_step_same; eauto with smallstep.
  rewrite (open_none ts); steps; eauto with wf.
Qed.

Lemma reducible_fix_strong_induction_aux:
  forall n ρ T tsv v ts,
    tree_size v < n ->
    fv T = nil ->
    fv ts = nil ->
    wf T 1 ->
    wf ts 1 ->
    is_nat_value v ->
    is_erased_term ts ->
    is_erased_type T ->
    valid_interpretation ρ ->
    notype_tfix ts ~>* tsv ->
    cbv_value tsv ->
    (forall tx n,
       [ ρ ⊨ n : T_nat ]v ->
       [ ρ ⊨ tx : T_forall (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) n)) T ]v ->
       [ tx ≡ notype_tfix ts ] ->
       [ ρ ⊨ open 0 ts tx : open 0 T n ]) ->
    [ ρ ⊨ notype_tfix ts : open 0 T v ].
Proof.
  induction n; repeat step || simp_red_goal || simp_red_top_level_hyp; try lia;
    eapply backstep_reducible;
      repeat step || list_utils;
      eauto using scbv_step_fix_open;
      eauto with wf.

  apply reducibility_equivalent2 with (open 0 (open 1 ts zero) tsv);
    repeat step || apply equivalent_context || apply_any || simp_red_goal || simp_red_top_level_hyp ||
           rewrite open_tlt in * ||
           rewrite (open_none ts) by (steps; unshelve eauto with wf; auto);
    try solve [ apply equivalent_sym; equivalent_star ];
    eauto 2 with wf fv erased step_tactic.

  - unfold closed_value, closed_term; steps;
      eauto using wf_star_smallstep with fv wf erased step_tactic.

  - apply reducible_expr_value; auto.
    apply reducibility_equivalent2 with (notype_tfix ts);
      try solve [ equivalent_star ];
      eauto 2 with wf fv erased step_tactic.

    apply IHn with tsv;
      repeat step || simp_red_goal || (rewrite tree_size_build_nat in *)
                  || simp_red_top_level_hyp
                  || last_step_binary_primitive
                  || rewrite open_none in * by t_closer;
      try solve [ unshelve t_closer; auto ];
      try lia.
Qed.

Lemma reducible_fix_strong_induction:
  forall ρ T v ts tsv,
    fv T = nil ->
    fv ts = nil ->
    wf T 1 ->
    wf ts 1 ->
    is_nat_value v ->
    is_erased_term ts ->
    is_erased_type T ->
    valid_interpretation ρ ->
    notype_tfix ts ~>* tsv ->
    cbv_value tsv ->
    (forall tx n,
       [ ρ ⊨ n : T_nat ]v ->
       [ ρ ⊨ tx : T_forall (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) n)) T ]v ->
       [ tx ≡ notype_tfix ts ] ->
       [ ρ ⊨ open 0 ts tx : open 0 T n ]) ->
    [ ρ ⊨ notype_tfix ts : open 0 T v ].
Proof.
  eauto using reducible_fix_strong_induction_aux.
Qed.

Lemma reducible_fix_strong_induction_forall:
  forall ρ ts tsv T,
    fv T = nil ->
    fv ts = nil ->
    wf T 1 ->
    wf ts 1 ->
    is_erased_term ts ->
    valid_interpretation ρ ->
    is_erased_type T ->
    notype_tfix ts ~>* tsv ->
    cbv_value tsv ->
    (forall tx n,
       [ ρ ⊨ n : T_nat ]v ->
       [ ρ ⊨ tx : T_forall (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) n)) T ]v ->
       [ tx ≡ notype_tfix ts ] ->
       [ ρ ⊨ open 0 ts tx : open 0 T n ]) ->
    [ ρ ⊨ notype_tfix ts : T_forall T_nat T ].
Proof.
  repeat step.

  apply reducible_forall with (open 0 T zero); steps;
    eauto using reducible_fix_zero.

  eapply reducible_fix_strong_induction; repeat step || simp_red_goal || simp_red_top_level_hyp;
   eauto with fv wf.
Qed.

Lemma open_reducible_fix_strong_induction:
  forall Θ ts Γ T n y p,
    wf T 1 ->
    wf ts 1 ->
    subset (fv T) (support Γ) ->
    subset (fv ts) (support Γ) ->
    ~(p ∈ fv T) ->
    ~(p ∈ fv_context Γ) ->
    ~(y ∈ fv ts) ->
    ~(y ∈ fv T) ->
    ~(y ∈ fv_context Γ) ->
    ~(n ∈ fv ts) ->
    ~(n ∈ fv T) ->
    ~(n ∈ fv_context Γ) ->
    is_erased_term ts ->
    is_erased_type T ->
    cbv_value ts ->
    NoDup (n :: y :: p :: nil) ->
    [ Θ;
        (p, T_equiv (fvar y term_var) (notype_tfix ts)) ::
        (y,
          (T_forall
             (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) (fvar n term_var)))
             T)
        ) ::
        (n, T_nat) ::
        Γ ⊨
      open 0 ts (fvar y term_var) : open 0 T (fvar n term_var) ] ->
    [ Θ; Γ ⊨ notype_tfix ts : T_forall T_nat T ].
Proof.
  unfold open_reducible in *; steps.

  apply reducible_fix_strong_induction_forall with
      (open 0 (psubstitute ts lterms term_var) (notype_tfix (psubstitute ts lterms term_var)));
        repeat step || apply star_one || apply scbv_step_fix_open ||
               apply cbv_value_open || apply cbv_value_subst;
    unshelve eauto with wf;
    eauto with fv;
    eauto with erased;
    try solve [ rewrite substitute_open2; eauto with wf ].

  unshelve epose proof (H15 ρ ((p, uu) :: (y, tx) :: (n, n0) :: lterms) _ _ _) as HH;
    repeat step || apply SatCons || nodup || rewrite pfv_tlt in * || rewrite pfv_shift2 in * || list_utils;
    eauto 2 with fv;
    eauto 2 with wf;
    eauto 2 with twf.

  - repeat step || t_substitutions || simp_red_goal.
  - repeat step || rewrite psubstitute_tlt in * || (rewrite substitute_shift in * by eauto 2 with wf step_tactic) || t_substitutions.
  - repeat step || t_substitutions || nodup.
Qed.

author: epfl-lara

repo: SystemFR

save_path: github-repos/coq/epfl-lara-SystemFR


text:
Require Import Coq.FSets.FMapPositive.
Require Import Rewriter.Util.Bool.Equality.
Require Import Rewriter.Util.Decidable.

Module PositiveMap.
  Scheme Induction for PositiveMap.tree Sort Type.
  Scheme Induction for PositiveMap.tree Sort Set.
  Scheme Induction for PositiveMap.tree Sort Prop.
  Scheme Equality for PositiveMap.tree.

  Notation t_beq := tree_beq.
  Notation t_eq_dec := tree_eq_dec.
  Notation internal_t_dec_bl := internal_tree_dec_bl.
  Notation internal_t_dec_lb := internal_tree_dec_lb.

  Lemma tree_eq_dec' {A} (A_dec : forall x y : A, {x = y} + {x <> y})
    : forall x y : PositiveMap.tree A, {x = y} + {x <> y}.
  Proof.
    intros; do 2 decide equality.
  Qed.

  Global Instance tree_dec_eq {A} {A_dec : DecidableRel (@eq A)}
    : DecidableRel (@eq (PositiveMap.tree A))
    := @tree_eq_dec' A A_dec.
  Global Instance t_dec_eq {A} {A_dec : DecidableRel (@eq A)}
    : DecidableRel (@eq (PositiveMap.t A))
    := @tree_eq_dec' A A_dec.
End PositiveMap.

author: mit-plv

repo: rewriter

save_path: github-repos/coq/mit-plv-rewriter