Library Sublogic

Require Export basic.
Require Import Logics.

Reserved Notation "# T" (at level 200).

Set Implicit Arguments.

1. Sublogics, wrapped in modules and functors

Module Type Sublogic.
  Parameter Inline Tr : Prop -> Prop.
  Parameter TrI : ∀ P:Prop, P -> Tr P.
  Parameter TrP : ∀ P:Prop, Tr (Tr P) -> Tr P.
  Parameter TrMono : ∀ (P Q:Prop), (P->Q)->Tr P->Tr Q.
  Notation "# T" := (Tr T).
End Sublogic.

Family of sublogic

Module Type SublogicFamily.
  Parameter T : Type.
  Parameter Inline Tr : T -> Prop -> Prop.
  Parameter TrI : ∀ x (P:Prop), P -> Tr x P.
  Parameter TrP : ∀ x (P:Prop), Tr x (Tr x P) -> Tr x P.
  Parameter TrMono : ∀ x (P Q:Prop), (P->Q)->Tr x P->Tr x Q.
End SublogicFamily.

Module Type Type_sig. Parameter T : Type. End Type_sig.
Module Type Elt_sig (T:Type_sig). Parameter x : T.T. End Elt_sig.

Module InstSublogicFamily (L:SublogicFamily) (X:Elt_sig L) <: Sublogic.
  Import X.
  Definition Tr := L.Tr x.
  Definition TrI := L.TrI x.
  Definition TrP := @L.TrP x.
  Definition TrMono := @L.TrMono x.
End InstSublogicFamily.

Module Type ConsistentSublogic.
Include Sublogic.
Parameter TrCons : ~ Tr False.
End ConsistentSublogic.

Sublogics are monads

Module AlternativeFormulations.

  Module Type LogicMonad.
    Parameter Inline M : Prop -> Prop.
    Parameter ret : ∀ P:Prop, P -> M P.
    Parameter bind : ∀ P Q:Prop, M P -> (P -> M Q) -> M Q.
  End LogicMonad.

  Module SublogicToMonad (M:LogicMonad) : Sublogic with Definition Tr := M.M.
    Import M.
    Definition Tr := M.
    Definition TrI (P:Prop) (p:P) : Tr P := ret p.
    Definition TrP (P:Prop) (p:Tr(Tr P)) : Tr P := bind p (fun x => x).
    Definition TrMono (P Q:Prop) (f:P->Q) (p:Tr P) : Tr Q :=
      bind p (fun x => ret (f x)).
  End SublogicToMonad.
  Module MonadToSublogic (L:Sublogic) : LogicMonad with Definition M := L.Tr.
    Import L.
    Definition M := Tr.
    Definition ret (P:Prop) (p:P) : M P := TrI p.
    Definition bind (P Q:Prop) (p:Tr P) (f:P->Tr Q) : Tr Q :=
      TrP (TrMono f p).
  End MonadToSublogic.

End AlternativeFormulations.

Sublogic equipped with tools useful for doing logics

Module Type SublogicTheory.

Include Sublogic.

Definition isL (P:Prop) := Tr P -> P.

Global Instance Tr_morph : Proper (iff ==>iff) Tr.
Admitted.
Global Instance isL_morph : Proper (iff ==>iff) isL.
Admitted.

Parameter TrB : ∀ (P Q:Prop), Tr P -> (P -> Tr Q) -> Tr Q.
Parameter Tr_ind : ∀ (P Q:Prop) {i:isL Q}, (P -> Q) -> Tr P -> Q.

The set of L-propositions: introduction rules

  Parameter Tr_isL : ∀ P, isL (Tr P).
  Parameter T_isL : ∀ P:Prop, P -> isL P.
  Parameter and_isL : ∀ P Q, isL P -> isL Q -> isL (P /\Q).
  Parameter fa_isL : ∀ A (P:A->Prop),
    (∀ x, isL (P x)) -> isL(∀ x, P x).
  Parameter imp_isL : ∀ P Q, isL Q -> isL (P -> Q).
  Parameter iff_isL : ∀ P Q, isL P -> isL Q -> isL (P <-> Q).

Global Hint Resolve Tr_isL T_isL and_isL fa_isL imp_isL iff_isL.

  Parameter rFF : ∀ (Q:Prop), Tr False -> Tr Q.
  Parameter rFF': ∀ (Q:Prop), Tr False -> isL Q -> Q.

Introduction tactics

Ltac Tin := apply TrI.
Ltac Texists t := Tin; exists t.
Ltac Tleft := Tin; left.
Ltac Tright := Tin; right.

Elimination tactics:

Tabsurd replaces the current goal with Tr False (ex-falso)
Telim H implements rules H:Tr P |- G --> |- P->G when G is a L-prop
Tdestruct H is the equivalent of destruct on a hypothesis Tr(Ind x). The goal shall be an L-prop

Ltac prove_isL :=
  intros;
  lazymatch goal with
  | |- isL(Tr _) => apply Tr_isL
  | |- isL(_ /\ _) => apply and_isL; prove_isL
  | |- isL True => apply T_isL; exact I
  | |- isL(impl _ _) => apply imp_isL; prove_isL
  | |- isL(iff _ _) => apply iff_isL; prove_isL
  | |- isL(_ -> _) => apply imp_isL; prove_isL
  | |- isL(∀ x, _) => apply fa_isL; intro; prove_isL
  | |- isL _ => auto 10; fail "Cannot prove isL side-condition"
  | |- _ => fail "Tactic prove_isL does not apply to this goal"
  end.

Ltac Tabsurd :=
  lazymatch goal with
  | |- Tr _ => apply rFF
  | |- _ => apply rFF';[|auto 10;fail"Cannot prove isL side-condition"]
  end.
Ltac Telim H :=
  lazymatch goal with
  | |- Tr _ => apply TrB with (1:=H); try clear H
  | |- _ => apply Tr_ind with (3:=H);[auto 10;fail"Cannot prove isL side-condition"|]; try clear H
  end.
Tactic Notation "Tdestruct" constr(H) :=
  Telim H; destruct 1.
Tactic Notation "Tdestruct" constr(H) "as" simple_intropattern(p) :=
  Telim H; intros p.

End SublogicTheory.

Module BuildLogic (L:Sublogic) <: SublogicTheory.

Include L.

Derived sublogic concepts:

more elimination rules (bind of the monad)
the set of L-propositions

Global Instance Tr_morph : Proper (iff ==>iff) Tr.
split; apply TrMono; apply H.
Qed.

Definition isL (P:Prop) := Tr P -> P.

Global Instance isL_morph : Proper (iff ==>iff) isL.
do 2 red; intros.
unfold isL; rewrite H; reflexivity.
Qed.

Lemma TrB : ∀ (P Q:Prop), Tr P -> (P -> Tr Q) -> Tr Q.
intros.
apply TrP; revert H; apply TrMono; auto.
Qed.

Lemma Tr_ind : ∀ (P Q:Prop) {i:isL Q}, (P -> Q) -> Tr P -> Q.
intros.
apply i; revert H0; apply TrMono; trivial.
Qed.

The set of L-propositions: introduction rules. L-props are closed under all connectives of negative polarity.

Lemma Tr_isL : ∀ P, isL (Tr P).
Proof TrP.

Lemma T_isL : ∀ P:Prop, P -> isL P.
Proof (fun _ p _ => p).

Lemma and_isL : ∀ P Q, isL P -> isL Q -> isL (P /\Q).
compute; intros.
split; revert H1; apply Tr_ind; firstorder.
Qed.

Lemma fa_isL : ∀ A (P:A->Prop),
(∀ x, isL (P x)) -> isL(∀ x, P x).
compute; intros.
revert H0; apply Tr_ind; firstorder.
Qed.

Lemma imp_isL : ∀ P Q, isL Q -> isL (P -> Q).
intros.
apply fa_isL; trivial.
Qed.

Lemma iff_isL : ∀ P Q, isL P -> isL Q -> isL (P <-> Q).
intros; apply and_isL; apply imp_isL; trivial.
Qed.

Global Hint Resolve Tr_isL T_isL and_isL fa_isL imp_isL iff_isL.

Elimination rules for falsity

Lemma rFF (Q:Prop) : Tr False -> Tr Q.
apply TrMono; intros; contradiction.
Qed.
Lemma rFF' (Q:Prop) : Tr False -> isL Q -> Q.
intros.
apply H0; apply rFF; trivial.
Qed.

End BuildLogic.

The same for consistent logics: False is now an L-prop

Module BuildConsistentSublogic (L:ConsistentSublogic).
Module tmp <: SublogicTheory := BuildLogic L.
Include tmp.

Lemma FF_isL : isL False.
Proof L.TrCons.

Global Hint Resolve FF_isL.

End BuildConsistentSublogic.

2.Examples of sublogic modules

Coq's intuitionistic logic

Module CoqSublogic <: ConsistentSublogic.
Definition Tr P:Prop := P.
Definition TrI (P:Prop) (p:P) : Tr P := p.
Definition TrP (P:Prop) (p:Tr (Tr P)) : Tr P := p.
Definition TrMono (P Q:Prop) (f:P->Q) (p:Tr P) : Tr Q := f p.
Definition TrCons : ~ Tr False := fun h => h.
End CoqSublogic.

Module CoqSublogicThms := BuildConsistentSublogic CoqSublogic.

Classical logic through negated translation

Module ClassicSublogic <: ConsistentSublogic.
Definition Tr (P:Prop) := ~~P.
Definition TrI (P:Prop) (p:P) : Tr P := fun np => np p.
Definition TrP (P:Prop) (nnnnp:Tr (Tr P)) : Tr P :=
fun np => nnnnp (fun nnp => nnp np).
Definition TrMono (P Q:Prop) (f:P->Q) (nnp:Tr P) : Tr Q :=
fun nq => nnp (fun p => nq (f p)).
Definition TrCons : ~ Tr False := fun h => h (fun x => x).
End ClassicSublogic.

Module ClassicSublogicThms.
Include BuildConsistentSublogic ClassicSublogic.

Lemma nnpp (P:Prop) : ((P->False)->False) -> Tr P.
Proof (fun h => h).

excluded-middle: note that P need not be classical, which makes the positive case stronger.

Lemma classic : ∀ P, Tr(P \/ (Tr P -> False )).
intros P nem.
apply nem; right; intro tp.
apply Tr_ind with (3:=tp); intros; trivial.
apply nem; left; assumption.
Qed.
End ClassicSublogicThms.

Friedman's A-translation

Module ASublogic <: SublogicFamily.
  Definition T:=Prop.
  Definition Tr A P := P \/ A.
  Definition TrI (A P:Prop) (p:P) : Tr A P := or_introl p.
  Definition TrP (A P:Prop) (p:(P \/A )\/A) :=
    match p with
    | or_introl p => p
    | or_intror a => or_intror a
    end.
  Definition TrMono (A P Q:Prop) (f:P->Q) (p:P \/A) :=
    match p with
    | or_introl p => or_introl (f p)
    | or_intror a => or_intror a
    end.
End ASublogic.

Module Type Aprop. Parameter x:Prop. End Aprop.

Module ASublogicThms (A:Aprop) <: SublogicTheory.
  Module Asl := InstSublogicFamily ASublogic A.
  Import Asl.
  Notation A := A.x.
  Include BuildLogic Asl.

Lemma Aconsistency : isL False <-> ~A.
firstorder.
Qed.

Lemma atom_isL (P:Prop) : (A->P) -> isL P.
firstorder.
Qed.

or does not need to be modified

Lemma or_isL P Q : isL P \/ isL Q -> isL (P \/Q).
firstorder.
Qed.
Global Hint Resolve or_isL.

existential does need to be modified when one of the instances is an L-prop.

Lemma ex_isL_raw T (P:T->Prop):
(exists x, isL (P x)) -> isL(ex P).
firstorder.
Qed.

A more usable rule (we can expect the forall x, isL (P x) assumption to be provable automatically), but which requires T to be inhabited.

Lemma ex_isL T (P:T->Prop) :
T -> (∀ x, isL (P x)) -> isL (ex P).
compute; intros.
destruct H0; trivial.
exists X; auto.
Qed.
Global Hint Resolve ex_isL.

Lemma FF_a : Tr False <-> A.
split.
destruct 1;[contradiction|trivial].
right; trivial.
Qed.

End ASublogicThms.

Example: if ~~exists x. P(x) is derivable, then so is exists x. P(x)

Module AtransExample.
Parameter (T:Type) (P : T->Prop).
Module nnex. Definition x:=exists x, P x. End nnex.
Module Atr := ASublogicThms nnex.
Import nnex Atr.

Lemma markov_rule :
((Tr(exists x, P x) -> Tr False) -> Tr False) ->
exists x, P x.
intro.
apply FF_a.
apply H; intro.
apply Tr_ind with (3:=H0); intros; trivial.
apply Atr.Tr_isL.
apply FF_a.
assumption.
Qed.
End AtransExample.

Peirce translation

Module PeirceTrans <: SublogicFamily.
  Definition T := Prop.
  Definition Tr (R A:Prop) := (A->R)->A.
  Definition TrI (R A:Prop) (a:A) : Tr R A := fun ar => a.
  Definition TrP (R A:Prop) (tta:Tr R (Tr R A)) : Tr R A :=
   fun ar => tta (fun ara => ar (ara ar)) ar.
  Definition TrMono (R A B:Prop) (f:A->B) (ta:Tr R A) : Tr R B :=
   fun br => f (ta (fun a => br (f a))).
  Definition TrCons (R:Prop) : ~ Tr R False :=
   fun frf => frf (False_ind R).
End PeirceTrans.

Module PeirceSublogicThms (A:Aprop) <: SublogicTheory.
  Module Psl := InstSublogicFamily PeirceTrans A.
  Import Psl.
  Notation A := A.x.
  Include BuildLogic Psl.

Lemma Pconsistency : isL False.
firstorder.
Qed.

End PeirceSublogicThms.

Intersection and cartesian product

Module Inter (L:SublogicFamily) <: Sublogic.
  Definition Tr P := ∀ x, L.Tr x P.
  Definition TrI (P:Prop) (p:P) : Tr P := fun x => L.TrI x p.
  Definition TrP (P:Prop) (ttp:Tr(Tr P)) : Tr P :=
    fun x => L.TrP (L.TrMono (fun p => p x) (ttp x)).
  Definition TrMono (P Q:Prop) (f:P->Q) (p:Tr P) : Tr Q :=
    fun x => L.TrMono f (p x).
  Lemma equiCons : Tr False <-> ∀ x, L.Tr x False.
    reflexivity.
  Qed.
End Inter.

Module Inter2 (L1 L2:Sublogic) <: Sublogic.
  Definition Tr P := L1.Tr P /\ L2.Tr P.
  Definition TrI (P:Prop) (p:P) : Tr P := conj (L1.TrI p) (L2.TrI p).
  Definition TrP (P:Prop) (ttp:Tr(Tr P)) : Tr P :=
    conj (L1.TrP (L1.TrMono (fun p => proj1 p) (proj1 ttp)))
         (L2.TrP (L2.TrMono (fun p => proj2 p) (proj2 ttp))).
  Definition TrMono (P Q:Prop) (f:P->Q) (p:Tr P) : Tr Q :=
    conj (L1.TrMono f (proj1 p)) (L2.TrMono f (proj2 p)).
  Lemma equiCons : Tr False <-> L1.Tr False /\ L2.Tr False.
    reflexivity.
  Qed.
  Lemma isL_intro P : (L1.Tr P -> P ) \/ (L2.Tr P -> P ) -> (Tr P -> P).
destruct 1; destruct 1; auto.
Qed.

End Inter2.

3. Building a higher-order logic with L-props.

Module SublogicToHOLogic (L:SublogicTheory) <: HOLogic.
Import L.

Record prop_ := mkP { holds : Prop; isprop : isL holds }.
Definition prop := prop_.

Definition TT : prop.
exists True; auto.
Defined.
Definition FF : prop.
exists (Tr False); trivial.
Defined.
Definition Imp (P Q:prop) : prop.
exists (holds P->holds Q).
apply imp_isL; apply isprop.
Defined.
Definition Not p := Imp p FF.
Definition And (P Q:prop) : prop.
exists (holds P /\ holds Q).
apply and_isL; apply isprop.
Defined.
Definition Or (P Q:prop) : prop.
exists (Tr(holds P \/ holds Q)).
trivial.
Defined.
Definition Forall {A} (P:A->prop) : prop.
exists (∀ x, holds (P x)).
apply fa_isL; intros x; apply isprop.
Defined.
Definition Exist {A} (P:A->prop) : prop.
exists (Tr(exists x, holds (P x))).
trivial.
Defined.
Definition Ex2 {A} (P Q:A->prop) : prop.
exists (Tr(exists2 x, holds (P x) & holds (Q x))).
trivial.
Defined.

Inference rules

Lemma rTT : holds TT.
exact I.
Qed.
Lemma rFF P : holds FF -> holds P.
simpl.
apply Tr_ind; [apply isprop|contradiction].
Qed.
Lemma rAnd P Q : holds (And P Q) <-> holds P /\ holds Q.
reflexivity.
Qed.
Lemma rImp P Q : holds (Imp P Q) <-> (holds P -> holds Q ).
reflexivity.
Qed.
Lemma rForall A P : holds (Forall P) <-> ∀ x:A, holds (P x).
reflexivity.
Qed.
Lemma rNot P : holds (Not P) <-> (holds P -> holds FF ).
reflexivity.
Qed.
Lemma rOrI P Q : holds P \/ holds Q -> holds (Or P Q).
simpl.
apply TrI.
Qed.
Lemma rOrE P Q C : (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
intro; apply Tr_ind; [apply isprop|trivial].
Qed.
Lemma rExI A P : (exists (x:A ), holds (P x)) -> holds (Exist P).
destruct 1; simpl; apply TrI; eauto.
Qed.
Lemma rExE A P C : (∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
intro; apply Tr_ind; [apply isprop|].
destruct 1; eauto.
Qed.
Lemma rEx2I A (P Q:A->prop) : (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
destruct 1; simpl; apply TrI; eauto.
Qed.
Lemma rEx2E A P Q C : (∀ x:A, holds (P x) -> holds (Q x) -> holds C) -> holds (Ex2 P Q) -> holds C.
intro; apply Tr_ind; [apply isprop|].
destruct 1; eauto.
Qed.

Lemma equiCons : Tr False <-> holds FF.
reflexivity.
Qed.

End SublogicToHOLogic.