% File: sound.elf

% Translation of classical derivations to intuitionistic derivations of transformed formula.

% (Soundness)   
% (Gamma = a1:i,...,an:i,p1:o,...,pm:o
%  Kappa = kolm p1 - - p1,...,kolm pm - - pm
%  Psi   = nk A1,...,nk Ak
%  Psi*  = nj A1*,...,nj Ak*
%
% Given: Gamma,Psi |- NK::nk A
%        Gamma,Kappa |- sound Ai Ai' for i = 1,...,k.
%    and Gamma,Kappa |- K::kolm A A*
%
% Then we have NJ such that
% Gamma,Psi* |- NJ::nj A*

% The induction is on the classical natural deduction NK of A.

% Prover error: A proof could not be found
%theorem sound_auto : forall* {A:o} {A*:o} forall {NK:nk A} {K:kolm A A*} 
                       exists {NJ:nj A*} true.
% %prove 8 NK (sound_auto NK K NJ).

sound : nk A -> kolm A A* -> nj A* -> type.
%mode sound +NK +K -NJ.

% andi -- easy, andi and double negate
sound_andi     : sound (nk_andi NKA NKB) (kolm_and KB KA) 
                       (nj_dnotx (nj_andi NJA NJB))
    <- sound NKA KA NJA
    <- sound NKB KB NJB.

% This uses the following derivation from - - (- - A* and - - B*) to - - A*
%                   ------------------- v
%                    - - A+ and B*
%    ----------- u  ------------------- andel
%       - A+         - - A+
%     ------------------------ -E
%         p
%      ----------------------- -I^p^v        [hyp]
%       - (- - A+ and B*)             - - (- - A+ and B*)
%      ------------------------------------------------------- -E
%                        q
%                    --------- -I^q^u
%                     - - A+

sound_andel : sound (nk_andel (NK1:nk (A and B))) KA 
                    (nj_noti ([q:o] [u:nj (not A+)]
                      (nj_note NJ1 q
                        (nj_noti ([p:o] [v:nj ((n A+) and B*)]
                          (nj_note (nj_andel v) p u))))))
    <- existskolm B B* KB
    <- sound NK1 (kolm_and KB KA) NJ1.  % NJ1::- - (- - A+ and B*)

% as in previous case
sound_ander : sound (nk_ander (NK1:nk (A and B))) KB
                    (nj_noti ([q:o] [u:nj (not B+)]
                      (nj_note NJ1 q
                        (nj_noti ([p:o] [v:nj (A* and (n B+))]
                          (nj_note (nj_ander v) p u))))))
    <- existskolm A A* KA
    <- sound NK1 (kolm_and KB KA) NJ1.  % NJ1::- - (A* and - - B+)

% impi -- easy.  apply impi and double negate
sound_impi : sound (nk_impi NKB) (kolm_imp KB KA) 
                   (nj_dnotx (nj_impi NJB))
    <- ({u:nk A} {v:nj A*} sound u KA v ->
          sound (NKB u) KB (NJB v)).

% impe -- harder, same kind of playing with negation
% as in other cases.
sound_impe : sound (nk_impe NKI (NKA:nk A)) KB
                   (nj_noti [q:o] [v:nj (not B+)]
                     (nj_note NJI q 
                       (nj_noti [p:o] [u:nj (A* imp (n B+))]
                         (nj_note (nj_impe u NJA) p v))))
    <- existskolm A A* KA
    <- sound NKA KA NJA
    <- sound NKI (kolm_imp KB KA) NJI.

      
% or-introductions are easy, we simply apply or-intro and double negate
sound_oril : sound (nk_oril NK) (kolm_or KB KA)
                   (nj_dnotx (nj_oril NJ))
    <- sound NK KA NJ.

sound_orir : sound (nk_orir NK) (kolm_or KB KA)
                   (nj_dnotx (nj_orir NJ))
    <- sound NK KB NJ.

%                     ------     ------
%                       A*       B*
%  ---------------- u . . .      . . .
%     A* or B*        - - C+    - - C+
%  ------------------------------------ ore
%                     
%    ---- v           - - C+
%    - C+
%    --------------------------- note
%                            p
%    [hyp]                ------------------- noti^p^u
%  - -(A* or B*)          -(A* or B*) 
%  ------------------------------------------ note
%                        q
%  ------------------------------------------ noti^q^v
%                  - - C+
sound_ore  : sound (nk_ore (NK:nk (A or B)) NKA NKB) KC 
                   (nj_noti [q:o] [v:nj (not C+)]
                     (nj_note NJ q 
                       (nj_noti [p:o] [u:nj (A* or B*)]
                         (nj_note (nj_ore u NJA NJB) p v))))
    <- existskolm A A* KA
    <- existskolm B B* KB
    <- sound NK (kolm_or KB KA) NJ
    <- ({u:nk A} {v:nj A*} sound u KA v ->
          sound (NKA u) KC (NJA v))
    <- ({u:nk B} {v:nj B*} sound u KB v ->
          sound (NKB u) KC (NJB v)).

% noti -- use Lemma 2 (nj_dneg_falser)  - - false |- q
sound_noti : sound (nk_noti NK1) (kolm_not K)
                   (nj_dnotx 
                     (nj_noti ([q] [v:nj A*]
                       (nj_dneg_falser (NJ1 false v) q))))
    <- ({p} {u:nk A} {v:nj A*} {kp:kolm p (n p)} 
        existskolm p (n p) kp ->
        sound u K v ->
         sound (NK1 p u) kp (NJ1 p v)). % (NJ1 p v):nj (n p)

% note -- use Lemma 1 to derive - - - A from - - - - - A
% and apply note
sound_note : sound (nk_note NK2 C (NK1:nk A)) KC 
                   (nj_note (nj_triple_neg_red NJ2)
                            (n C*) NJ1)
      <- existskolm A A* KA
      <- sound NK2 (kolm_not KA) NJ2
      <- sound NK1 KA NJ1.

% truei -- easy!
sound_truei : sound nk_truei kolm_true (nj_dnotx nj_truei).

% falsee -- Use Lemma 2
sound_falsee : sound (nk_falsee NK) KC
                     (nj_dneg_falser NJ C*)
    <- sound NK kolm_false NJ.

% foralli -- easy, foralli and double negate
sound_foralli : sound (nk_foralli NK) (kolm_forall KA)
                      (nj_dnotx (nj_foralli NJ))
    <- ({a:i} sound (NK a) (KA a) (NJ a)).

% foralle -- hard -- play with negations as usual
sound_foralle : sound (nk_foralle NK T) (KA T)
                      (nj_noti [q:o] [v:nj (not (A+ T))]
                        (nj_note NJ q
                          (nj_noti [p:o] [u:nj (forall ([x:i] (n (A+ x))))]
                            (nj_note (nj_foralle u T) p v))))
    <- existskolm (forall A) (n (forall ([x] (n (A+ x)))))
                  (kolm_forall KA)
    <- sound NK (kolm_forall KA) NJ.

% existsi -- easy, existsi and double negate
sound_existi : sound (nk_existsi T NK) (kolm_exists KA) 
                     (nj_dnotx (nj_existsi T NJ))
    <- sound NK (KA T) NJ.

% existse -- hard -- play around with negations (compare to ore)
sound_existse : sound (nk_existse (NKEA:nk (exists A)) NKC) KC 
                      (nj_noti [q:o] [v:nj (not C+)]
                        (nj_note NJnnEA q
                          (nj_noti [p:o] [u:nj (exists A*)]
                            (nj_note (nj_existse u NJC) p v))))
    <- existskolm (exists A) (n (exists A*))
                  (kolm_exists KA)
    <- sound NKEA (kolm_exists KA) NJnnEA
    <- ({a:i} {u:nk (A a)} {v:nj (A* a)}
         sound u (KA a) v ->
           sound (NKC a u) KC (NJC a v)).

% dnotr (excluded middle as the inference rule - - A |- A)
% Here we have KA : kolm A A*
% and NK:nk (n A) (by inversion)
% By induction (applied to NK) and inversion on K
% we have NJ:nj (n not (n not (n A+)))
% Apply the argument above to obtain NJ':nj (n n n A+)
% and again to obtain NJ'':nj (n n A+)
% and finally to obtain NJ''':nj (n A+)
% and that's what we want!
sound_dnotr    : sound (nk_dnotr NK1) KA
                       (nj_triple_neg_red
                          (nj_triple_neg_red
                             (nj_triple_neg_red NJ1)))
    <- sound NK1 (kolm_not (kolm_not KA)) NJ1.



%block l1 : block {a:i}.
%block l2 : some {A:o}{A*:o} block {NK': nk A}{K':kolm A A*}{NJ':nj A*}.
%block l3 : some {A:o}{A*:o}{KA:kolm A A*}
	     block {u:nk A} {v:nj A*} {h:sound u KA v}.

%block l4 : some  {A:o} {A*:o} {K: kolm A A*}
	     block {p : o} {u:nk A} {v:nj A*} {kp:kolm p (n p)}
	     {h1 : existskolm p (n p) kp}
	     {h2 : sound u K v}.


%mode (kolm +A -A*).
%worlds (l1 | l2 | l3 | l4) (kolm _ _).
%total A (kolm A A*).

%worlds (l1 | l2 | l3 | l4) (existskolm _ _ _).
%total A (existskolm A A* K).

%terminates NK (sound NK K NJ).
%mode (sound +NK +K -NJ).
%worlds (l1 | l3 | l4) (sound _ _ _).
% %covers (sound +NK +K -NJ).    % it really doesn't seem to cover check! --cs