Coq AR Ex 4.4

(* basic.v *)
Require Import List Lia.
Require Import String.
Import ListNotations Nat.
Open Scope string.
Open Scope nat_scope.

Ltac inv H := inversion H; subst; clear H.

Inductive formula {Pi} :=
  Bot | Top | V (p:Pi) | Not (a:formula) |
  And (a b:formula) | Or (a b:formula) |
  To (a b:formula) | Equiv (a b:formula).

Notation "F ∨ G" := (Or F G)(at level 71).
Notation "F ∧ G" := (And F G)(at level 71).
Notation "F → G" := (To F G)(at level 71).
Notation "F ↔ G" := (Equiv F G)(at level 71).
Notation "¬ F" := (Not F)(at level 70).
Notation "x ∈ xs" := (xs x)(at level 80, only parsing).
Notation "T 'set'" := (T -> Prop)(at level 80, only parsing).

Definition StringVar := @V string.
Coercion StringVar : string >-> formula.

Definition bool2nat (b:bool) := if b then 1 else 0.
Coercion bool2nat : bool >-> nat.

Inductive polarity := TT | FF | NN.



(* functions.v *)

Definition app {X} {Y} (f:X->Y) (x:option X) : option Y :=
  match x with
    None => None
  | Some x => Some (f x)
  end.

Fixpoint subst {Pi} (F G:@formula Pi) p :=
  match F, p with
    _, [] => Some G
  | (Not F), 1::p => app Not (subst F G p)
  | (And F1 F2), 1::p => app (fun f => And f F2) (subst F1 G p)
  | (And F1 F2), 2::p => app (And F1) (subst F2 G p)
  | (Or F1 F2), 1::p => app (fun f => Or f F2) (subst F1 G p)
  | (Or F1 F2), 2::p => app (Or F1) (subst F2 G p)
  | (To F1 F2), 1::p => app (fun f => To f F2) (subst F1 G p)
  | (To F1 F2), 2::p => app (To F1) (subst F2 G p)
  | (Equiv F1 F2), 1::p => app (fun f => Equiv f F2) (subst F1 G p)
  | (Equiv F1 F2), 2::p => app (Equiv F1) (subst F2 G p)
  | _, _ => None
  end.

Definition negPol p :=
  match p with
    TT => FF
  | FF => TT
  | NN => NN
  end.

Fixpoint pol {Pi} (F:@formula Pi) p :=
  match F,p with
    _, [] => Some TT
  | (Not F), 1::p => app negPol (pol F p)
  | (And F1 F2), 1::p => pol F1 p
  | (And F1 F2), 2::p => pol F2 p
  | (Or F1 F2), 1::p => pol F1 p
  | (Or F1 F2), 2::p => pol F2 p
  | (To F1 F2), 1::p => app negPol (pol F1 p)
  | (To F1 F2), 2::p => pol F2 p
  | (Equiv F1 F2), 1::p => Some NN
  | (Equiv F1 F2), 2::p => Some NN
  | _,_ => None
  end.

Fixpoint eval {Pi} (A:Pi->bool) (F:@formula Pi) : nat :=
  match F with
    Bot => 0
  | Top => 1
  | V p => A p
  | Not F => 1-eval A F
  | And F G => min (eval A F) (eval A G)
  | Or F G => max (eval A F) (eval A G)
  | To F G => max (1-eval A F) (eval A G)
  | Equiv F G => if eval A F =? eval A G then 1 else 0
  end.

Definition sat {Pi} A (F:@formula Pi) : Prop := eval A F = 1.

Definition satisfiable {Pi} (F:@formula Pi) : Prop :=
  exists A, sat A F.



(* properties.v *)

Lemma polEmpty {Pi} (H:@formula Pi) : pol H [] = Some TT.
Proof.
  destruct H;reflexivity.
Qed.

Lemma substEmpty {Pi} (H F:@formula Pi) : subst H F [] = Some F.
Proof.
  destruct H;reflexivity.
Qed.

Lemma appInv {X Y} (f:X->Y) x b: app f x = Some b <-> exists a, x=Some a /\ b=f a.
Proof.
  unfold app.
  split.
  - intros H. destruct x.
    + exists x;split;congruence.
    + congruence.
  - intros (a&H0&H1). now subst.
Qed.

Lemma evalDestruct {Pi} (A:Pi->bool) F: eval A F = 0 \/ eval A F = 1.
Proof.
  induction F;cbn.
  all: try (destruct IHF1 as [->| ->], IHF2 as [-> | ->];cbn;tauto).
  - now left.
  - now right.
  - destruct A;tauto.
  - destruct eval;tauto.
Qed.

Lemma evalInd {Pi} (A:Pi->bool) F (p:nat->Prop): (eval A F = 0 -> p 0) -> (eval A F = 1 -> p 1) -> forall b, eval A F = b -> p b.
Proof.
  intros.
  destruct (evalDestruct A F);subst;rewrite H2;eauto.
Qed.


(* poscomb.v *)

Section poscomb.
  Variable (Π:Type).
  Implicit Type (N:@formula Π set). (* Set of formulas (possible infinite) *)
  Definition satSet A N := forall F, F ∈ N -> sat A F.
  Definition satisfiableSet N := exists A, satSet A N.

  Inductive poscomb N : formula set :=
  | poscombBase F: F ∈ N -> F ∈ poscomb N
  | poscombAnd F F': F ∈ poscomb N -> F' ∈ poscomb N -> F ∧ F' ∈ poscomb N
  | poscombOr F F': F ∈ poscomb N -> F' ∈ poscomb N -> F ∨ F' ∈ poscomb N.

  Lemma poscombSat N A : satSet A N -> forall F, F ∈ poscomb N -> sat A F.
  Proof.
    intros H F.
    induction 1;unfold sat in *;cbn;try lia.
    now apply H in H0.
  Qed.

  Lemma L12 N: satisfiableSet N -> forall F, F ∈ poscomb N -> satisfiable F.
  Proof.
    intros [A H] F G. exists A.
    apply (poscombSat N A H F G).
  Qed.

End poscomb.