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
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. 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. 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. %% 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}. %% 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}. %% 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}. %% 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'}.