Require Import Arith.

Inductive bop := Band | Bor | Bimp.
Inductive rel := Neq | Nle | Nlt.

Inductive formula :=
  | Fbop : bop -> formula -> formula -> formula
  | Fnot : formula -> formula
  | Frel : rel -> nat -> nat -> formula.

Fixpoint interp_formula f :=
  match f with
  | Fbop o p q =>
    match o with
    | Band => and
    | Bor => or
    | Bimp => fun p q => p -> q
    end (interp_formula p) (interp_formula q)
  | Fnot p => not (interp_formula p)
  | Frel r m n =>
    match r with
    | Neq => @eq nat
    | Nle => le
    | Nlt => lt
    end m n
  end.

Ltac reify_formula f :=
  match f with
  | ?p -> ?q =>
    let p' := reify_formula p in
    let q' := reify_formula q in
    constr:(Fbop Bimp p' q')
  | ?p /\ ?q =>
    let p' := reify_formula p in
    let q' := reify_formula q in
    constr:(Fbop Band p' q')
  | ?p \/ ?q =>
    let p' := reify_formula p in
    let q' := reify_formula q in
    constr:(Fbop Bor p' q')
  | not ?p =>
    let p' := reify_formula p in
    constr:(Fnot p')
  | ?r ?m ?n =>
    let r' := match r with @eq nat => Neq | le => Nle | lt => Nlt end in
    constr:(Frel r' m n)
  end.

Definition imp_bool (p q : bool) :=
  if q then true else if p then false else true.

Lemma imp_bool_correct :
  forall p q : bool, imp_bool p q = true <->
  (p = true -> q = true).
Proof.
intros [|] [|] ; split ; try easy.
intros H.
now discriminate H.
Qed.

Definition and_bool (p q : bool) :=
  if p then q else false.

Lemma and_bool_correct :
  forall p q : bool, and_bool p q = true <->
  (p = true /\ q = true).
Proof.
intros [|] [|] ; now split.
Qed.

Definition or_bool (p q : bool) :=
  if p then true else q.

Lemma or_bool_correct :
  forall p q : bool, or_bool p q = true <->
  (p = true \/ q = true).
Proof.
intros [|] [|] ; split ; try easy.
now left.
now left.
now right.
now intros [H|H].
Qed.

Definition not_bool (p : bool) :=
  if p then false else true.

Lemma not_bool_correct :
  forall p : bool, not_bool p = true <->
  not (p = true).
Proof.
intros [|] ; split ; try easy.
intros H.
now elim H.
Qed.

Fixpoint le_bool (m n : nat) :=
  match m, n with
  | 0, _ => true
  | S _, 0 => false
  | S m, S n => le_bool m n
  end.

Lemma le_bool_correct :
  forall m n, le_bool m n = true <-> m <= n.
Proof.
induction m.
intros [|n].
now split.
split ; intros _.
apply le_O_n.
apply refl_equal.
intros [|n].
now split.
split ; intros H.
apply le_n_S.
now apply -> IHm.
apply <- IHm.
now apply le_S_n.
Qed.

Fixpoint lt_bool (m n : nat) :=
  match m, n with
  | _, 0 => false
  | 0, S _ => true
  | S m, S n => lt_bool m n
  end.

Lemma lt_bool_correct :
  forall m n, lt_bool m n = true <-> m < n.
Proof.
induction m.
intros [|n].
now split.
split ; intros _.
apply lt_O_Sn.
apply refl_equal.
intros [|n].
now split.
split ; intros H.
apply lt_n_S.
now apply -> IHm.
apply <- IHm.
now apply lt_S_n.
Qed.

Fixpoint eq_bool (m n : nat) :=
  match m, n with
  | O, O => true
  | S m, S n => eq_bool m n
  | _, _ => false
  end.

Lemma eq_bool_correct :
  forall m n, eq_bool m n = true <-> m = n.
Proof.
induction m.
intros [|n].
now split.
now split.
intros [|n].
now split.
split ; intros H.
apply f_equal.
now apply -> IHm.
apply <- IHm.
now injection H.
Qed.

Fixpoint bool_formula f :=
  match f with
  | Fbop o p q =>
    match o with Band => and_bool | Bor => or_bool | Bimp => imp_bool end
    (bool_formula p) (bool_formula q)
  | Fnot p => not_bool (bool_formula p)
  | Frel r m n =>
    match r with Neq => eq_bool | Nle => le_bool | Nlt => lt_bool end m n
  end.

Theorem bool_formula_correct :
  forall f, bool_formula f = true <-> interp_formula f.
Proof.
induction f.
case b ; simpl ; rewrite <- IHf1, <- IHf2.
apply and_bool_correct.
apply or_bool_correct.
apply imp_bool_correct.
simpl.
rewrite <- IHf.
apply not_bool_correct.
case r.
apply eq_bool_correct.
apply le_bool_correct.
apply lt_bool_correct.
Qed.

Lemma bool_formula_classic :
  forall f, bool_formula (Fbop Bimp (Fnot f) f) = true -> bool_formula f = true.
Proof.
intros f.
simpl.
now case (bool_formula f).
Qed.

Ltac double_negate :=
  match goal with
  | |- ?g => let f := reify_formula g in change (interp_formula f)
  end ;
  apply -> bool_formula_correct ;
  apply bool_formula_classic ;
  apply <- bool_formula_correct ;
  simpl.

Goal forall m n, m + n <= n -> m = 0 /\ 0 <= n.
intros m n.
double_negate.
Admitted.

Fixpoint simplify f (b : bool) :=
  match f with
  | Fbop Bimp p q =>
    if b then Fbop Band (simplify p false) (simplify q true)
    else Fbop Bor (simplify p true) (simplify q false)
  | Fbop Band p q =>
    if b then Fbop Bor (simplify p true) (simplify q true)
    else Fbop Band (simplify p false) (simplify q false)
  | Fbop Bor p q =>
    if b then Fbop Band (simplify p true) (simplify q true)
    else Fbop Bor (simplify p false) (simplify q false)
  | Fnot p => simplify p (not_bool b)
  | Frel r m n =>
    if b then
      match r with
      | Neq => Fnot f
      | Nle => Frel Nlt n m
      | Nlt => Frel Nle n m
      end
    else f
  end.

Lemma simplify_correct_aux :
  forall f b,
  bool_formula (simplify f b) = bool_formula (if b then Fnot f else f).
Proof.
induction f.
intros [|] ;
  destruct b ;
  simpl ; rewrite IHf1, IHf2 ; simpl ;
  now case (bool_formula f1) ; case (bool_formula f2).
intros [|] ;
  simpl ; rewrite IHf ; simpl ;
  now case (bool_formula f).
intros [|] ; try easy ;
  destruct r ; simpl.
apply refl_equal.
generalize (le_bool_correct n n0) (lt_bool_correct n0 n).
case (le_bool n n0) ; case (lt_bool n0 n) ; try easy.
intros (H1,_) (H2,_).
elim (lt_irrefl n).
apply le_lt_trans with n0.
now apply H1.
now apply H2.
intros (_,H1) (_,H2).
now case (le_lt_dec n n0).
generalize (le_bool_correct n0 n) (lt_bool_correct n n0).
case (le_bool n0 n) ; case (lt_bool n n0) ; try easy.
intros (H1,_) (H2,_).
elim (lt_irrefl n).
apply lt_le_trans with n0.
now apply H2.
now apply H1.
intros (_,H1) (_,H2).
now case (le_lt_dec n0 n).
Qed.

Theorem simplify_correct :
  forall f b,
  interp_formula (simplify f b) <-> interp_formula (if b then Fnot f else f).
Proof.
intros f b.
rewrite <- bool_formula_correct.
rewrite <- bool_formula_correct.
split ; intros H ; rewrite <- H.
apply sym_eq.
apply simplify_correct_aux.
apply simplify_correct_aux.
Qed.

Ltac classicify :=
  match goal with
  | |- ?g => let f := reify_formula g in change (interp_formula f)
  end ;
  apply (proj1 (simplify_correct _ false)) ;
  simpl.

Goal forall m n, m + n <= n -> m = 0 /\ 0 <= n.
intros m n.
classicify.
destruct m as [|m].
right ; split.
apply refl_equal.
apply le_O_n.
left.
rewrite plus_Snm_nSm.
apply lt_le_trans with (S n).
apply lt_n_Sn.
apply le_plus_r.
Qed.

Print Assumptions Unnamed_thm0.