# Executable Specification

[View equiv.sig] [View equiv.mod]
```sig equiv.

kind     form                    type.

type     imp                     form -> form -> form.

type     nd, hil, conc, hyp      form -> o.

```
```module equiv.

% Natural deduction
nd (imp A B) :- nd A => nd B.      % implies introduction
nd B :- nd (imp A B), nd A.        % implies elimination

% Hilbert calculus
hil (imp A (imp B A)).                                   % K combinator
hil (imp (imp A (imp B C)) (imp (imp A B) (imp A C))).   % S combinator
hil B :- hil (imp A B), hil A.                           % Modus ponens

%% Sequent calculus
conc A :- hyp A.                                     % init
conc B :- hyp A => conc B, conc A.                   % cut

conc (imp A B) :- hyp A => conc B.                   % impR
conc C :- hyp (imp A B), conc A, hyp B => conc C.    % impL

```

# Reasoning

[View equiv.thm]

Click on a command or tactic to see a detailed view of its use.

```Specification "equiv".

%% Contexts

Define ctxs : olist -> olist -> olist -> prop by
ctxs nil nil nil ;
ctxs (nd G :: L) (hyp G :: J) (hil G :: K) := ctxs L J K.

Theorem ctxs_member1 : forall L J K E,
ctxs L J K -> member E L ->
exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K.
induction on 2. intros. case H2.
case H1. search.
case H1. apply IH to H4 H3. search.
Theorem ctxs_member2 : forall L J K E,
ctxs L J K -> member E J ->
exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K.
induction on 2. intros. case H2.
case H1. search.
case H1. apply IH to H4 H3. search.
Theorem ctxs_member3 : forall L J K E,
ctxs L J K -> member E K ->
exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J.
induction on 2. intros. case H2.
case H1. search.
case H1. apply IH to H4 H3. search.

%% Natural deduction -> sequent calculus

Theorem nd_to_seq_ext : forall L J K G,
ctxs L J K -> {L |- nd G} -> {J |- conc G}.
induction on 2. intros. case H2.
apply IH to _ H3. search.
apply IH to H1 H3. apply IH to H1 H4. search.
apply ctxs_member1 to H1 H4. case H3. search.
Theorem nd_to_seq : forall G,
{nd G} -> {conc G}.
intros. apply nd_to_seq_ext to _ H1. search.

%% Sequent calculus -> hilbert calculus

Set witnesses on.
Theorem hil_deduction : forall L J K A B,
ctxs L J K ->
{K, hil A |- hil B} -> {K |- hil (imp A B)}.
induction on 2. intros. case H2.
search. % KK
search. % KS
apply IH to _ H3. apply IH to _ H4. search. % S(H4)(H5)
case H4.
case H3. search. % SKK
apply ctxs_member3 to H1 H5. case H3. search. % K(H3)Set witnesses off.

Theorem seq_to_hil_ext : forall L J K G,
ctxs L J K -> {J |- conc G} -> {K |- hil G}.
induction on 2. intros. case H2.
case H3. apply ctxs_member2 to H1 H5. case H4. search.
apply IH to _ H3. apply IH to H1 H4.
apply hil_deduction to _ H5. search.
apply IH to _ H3. apply hil_deduction to _ H4. search.
case H3. apply ctxs_member2 to H1 H7. case H6.
apply IH to H1 H4. apply IH to _ H5.
apply hil_deduction to _ H11. search.
apply ctxs_member2 to H1 H4. case H3.
Theorem seq_to_hil : forall G,
{conc G} -> {hil G}.
intros. apply seq_to_hil_ext to _ H1. search.

%% Hilbert calculus -> natural deduction

Theorem hil_to_nd_ext : forall L J K G,
ctxs L J K -> {K |- hil G} -> {L |- nd G}.
induction on 2. intros. case H2.
search.
% This hint/assertion speeds up search considerably
assert {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}.
search.
apply IH to H1 H3. apply IH to H1 H4. search.
apply ctxs_member3 to H1 H4. case H3. search.
Theorem hil_to_nd : forall G,
{hil G} -> {nd G}.
intros. apply hil_to_nd_ext to _ H1. search.

%% The general form of the Hilbert deduction theorem:
%%   if   {hil A1, hil A2, ..., hil An |- hil B}
%%   then {hil (imp A1 (imp A2 (imp ... (imp An B)...)))}

Define fold : olist -> form -> form -> prop by
fold nil B B ;
fold (hil A :: L) B B' := fold L (imp A B) B'.

Theorem hil_deduction_generalized : forall L J K B B',
ctxs L J K ->
fold K B B' -> {K |- hil B} -> {hil B'}.
induction on 2. intros. case H2.
search.
case H1.
apply hil_deduction to _ H3.
apply IH to _ H4 H6. search.
```