Require Import Coq.Logic.Classical_Prop.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.Base.

Local Open Scope logic_base.

Section ContextProperty.

Context {L: Language}.

Definition at_least (P cP: context -> Prop): Prop :=
  forall (Phi: context), cP Phi -> P Phi.

Lemma at_least_self: forall P, at_least P P.
Proof.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  intros.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  hnf; intros.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c0) *)
  auto.
Qed.

Lemma at_least_left: forall P cP1 cP2, at_least P cP1 -> at_least P (Intersection _ cP1 cP2).
Proof.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  intros.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  hnf in H |- *; intros.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c0) *)
  destruct H0; auto.
Qed.

Lemma at_least_right: forall P cP1 cP2, at_least P cP2 -> at_least P (Intersection _ cP1 cP2).
Proof.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  intros.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  hnf in H |- *; intros.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c0) *)
  destruct H0; auto.
Qed.

Definition maximal (P: context -> Prop): context -> Prop :=
  fun Phi => P Phi /\ forall Psi, P Psi -> Included _ Phi Psi -> Included _ Psi Phi.

Lemma sig_context_ext: forall (cP: context -> Prop) (Phi Psi: sig cP),
  (forall x, proj1_sig Phi x <-> proj1_sig Psi x) -> Phi = Psi.
Proof.
(* Goal: forall (cP : forall _ : @context L, Prop) (Phi Psi : @sig (@context L) cP) (_ : forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x)), @eq (@sig (@context L) cP) Phi Psi *)
  intros.
(* Goal: @eq (@sig (@context L) cP) Phi Psi *)
  pose proof Extensionality_Ensembles _ _ _ (conj (fun x => proj1 (H x)) (fun x => proj2 (H x))).
(* Goal: @eq (@sig (@context L) cP) Phi Psi *)
  destruct Psi as [Psi ?], Phi as [Phi ?].
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Phi c0) (@exist (@context L) cP Psi c) *)
  simpl in H0; subst.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c) *)
  pose proof proof_irrelevance _ c c0.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c) *)
  subst.
(* Goal: @eq (@sig (@context L) cP) (@exist (@context L) cP Psi c0) (@exist (@context L) cP Psi c0) *)
  auto.
Qed.

End ContextProperty.

Ltac solve_at_least :=
  solve [apply at_least_self | auto | apply at_least_left; solve_at_least | apply at_least_right; solve_at_least].

