Specification "dual".
Set subgoals off.
% Splitting relation on multisets
Define split : list pol -> list pol -> list pol -> prop by
split nil nil nil
; split (X::L) (X::K) M := split L K M
; split (X::L) K (X::M) := split L K M.
% The member-and-rest relation on context
Define mnr : pol -> list pol -> list pol -> prop by
mnr X (X::L) L
; mnr X (Y::L) (Y::K) := mnr X L K.
% The relation that holds when all members of a relation start with the ? modal
Define modals : list pol -> prop by
modals nil
; modals ((? B)::C) := modals C.
% The judgment that a context is provable in muMALL.
Type ts list pol -> prop. % Turnstyle
% The inference rules of muMALL as axioms (unproven theorems in Abella).
Theorem exchange : forall P Q L, ts (P::Q::L) -> ts (Q::P::L). skip.
Theorem parI : forall P Q C C', mnr (par P Q) C C' -> ts (P::Q::C') -> ts C. skip.
Theorem botI : forall C C', mnr bot C C' -> ts C' -> ts C. skip.
Theorem neqI : forall T S C C', mnr (neq T S) C C' -> ((T = S) -> ts C') -> ts C. skip.
Theorem withI : forall P Q C C', mnr (with P Q) C C' -> (ts (P::C') /\ (ts (Q::C'))) -> ts C. skip.
Theorem allI : forall B C C', mnr (all B) C C' -> (forall x, ts (B x::C')) -> ts C. skip.
Theorem nu1I : forall B T C C', mnr (nu1 B T) C C' ->
(exists S, ts ((S T)::C') /\
(forall S', ({dual (all S) (some S')}) -> (forall x, ts ((B S x)::(S' x)::nil)))) -> ts C. skip.
Theorem nu1Ix : forall B T C C', mnr (nu1 B T) C C' -> % Enter the dual expression directly.
(exists S S', ts ((S T)::C') /\ (forall x, ts ((B S x)::(S' x)::nil))) -> ts C. skip.
Theorem nu3I : forall B T R U C C', mnr (nu3 B T R U) C C' -> (exists S, ts ((S T R U)::C') /\
(forall S', {dual (all x\ all y\ all u\ S x y u) (all x\ all y\ all u\ S' x y u)} ->
(forall x y u, ts ((B S x y u)::(S' x y u)::nil)))) -> ts C. skip.
Theorem unfold1 : forall B T1 C C', mnr (nu1 B T1) C C' -> ts ((B (nu1 B) T1 )::C') -> ts C. skip.
Theorem unfold2 : forall B T1 T2 C C', mnr (nu2 B T1 T2) C C' -> ts ((B (nu2 B) T1 T2 )::C') -> ts C. skip.
Theorem unfold3 : forall B T1 T2 T3 C C', mnr (nu3 B T1 T2 T3) C C' -> ts ((B (nu3 B) T1 T2 T3)::C') -> ts C. skip.
Theorem mu1I : forall B T1 C C', mnr (mu1 B T1) C C' -> ts ((B (mu1 B) T1 )::C') -> ts C. skip.
Theorem mu2I : forall B T1 T2 C C', mnr (mu2 B T1 T2) C C' -> ts ((B (mu2 B) T1 T2 )::C') -> ts C. skip.
Theorem mu3I : forall B T1 T2 T3 C C', mnr (mu3 B T1 T2 T3) C C' -> ts ((B (mu3 B) T1 T2 T3)::C') -> ts C. skip.
Theorem tensorI : forall P Q C C' D D', mnr (tensor P Q) C C' -> split C' D D' -> ts (P::D) -> ts (Q::D') -> ts C. skip.
Theorem tensorIx : forall P Q C C', mnr (tensor P Q) C C' -> (exists D D', split C' D D' /\ ts (P::D) /\ ts (Q::D')) -> ts C. skip.
Theorem oplusI : forall P Q C C', mnr (oplus P Q) C C' -> (ts (P::C') \/ (ts (Q::C'))) -> ts C. skip.
Theorem someI : forall B C C', mnr (some B) C C' -> (exists x, ts (B x::C')) -> ts C. skip.
Theorem oneI : ts (one::nil). skip.
Theorem eqI : forall T, ts ((eq T T)::nil). skip.
Theorem mu0nu0a : forall B B', {dual (mu0 B) (nu0 B')} -> ts ((mu0 B)::(nu0 B')::nil). skip.
Theorem mu0nu0b : forall B B', {dual (nu0 B) (mu0 B')} -> ts ((nu0 B)::(mu0 B')::nil). skip.
Theorem mu1nu1a : forall B B' T, {dual (mu1 B T) (nu1 B' T)} -> ts ((mu1 B T)::(nu1 B' T)::nil). skip.
Theorem mu1nu1b : forall B B' T, {dual (mu1 B T) (nu1 B' T)} -> ts ((nu1 B T)::(mu1 B' T)::nil). skip.
Theorem mu2nu2a : forall B B' T1 T2, {dual (mu2 B T1 T2) (nu2 B' T1 T2)} -> ts ((mu2 B T1 T2)::(nu2 B' T1 T2)::nil). skip.
Theorem mu2nu2b : forall B B' T1 T2, {dual (mu2 B T1 T2) (nu2 B' T1 T2)} -> ts ((nu2 B T1 T2)::(mu2 B' T1 T2)::nil). skip.
Theorem mu3nu3a : forall B B' T1 T2 T3, {dual (mu3 B T1 T2 T3) (nu3 B' T1 T2 T3)} -> ts ((mu3 B T1 T2 T3)::(nu3 B' T1 T2 T3)::nil). skip.
Theorem mu3nu3b : forall B B' T1 T2 T3, {dual (nu3 B T1 T2 T3) (mu3 B' T1 T2 T3)} -> ts ((nu3 B T1 T2 T3)::(mu3 B' T1 T2 T3)::nil). skip.
Theorem ginit : forall B B', {dual B B'} -> ts (B::B'::nil). skip.
Theorem weaken : forall B C C', mnr (? B) C C' -> ts C' -> ts C. skip.
Theorem derelict : forall B C C', mnr (? B) C C' -> ts (B::C') -> ts C. skip.
Theorem contract : forall B C C', mnr (? B) C C' -> ts ((? B)::(? B)::C') -> ts C. skip.
Theorem promote : forall B C C', mnr (bang B) C C' -> modals C' -> ts (B::C') -> ts C. skip.
Theorem promotex : forall C, (exists B C', mnr (bang B) C C' /\ modals C' /\ ts (B::C')) -> ts C. skip.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% First prove that the general form of the initial rule is admissible.
Theorem initial : forall A B, {dual A B} -> ts (A :: B :: nil).
induction on 1. intros. case H1.
backchain botI. backchain oneI.
backchain botI. backchain oneI.
backchain neqI. intros. case H2. backchain eqI.
backchain neqI. intros. case H2. backchain eqI.
backchain parI. backchain tensorIx. witness D::nil. witness E::nil. split.
search. apply IH to H2. search. apply IH to H3. search.
backchain parI. backchain tensorIx. witness B1::nil. witness C::nil. split.
search. apply IH to H2. backchain exchange. apply IH to H3. backchain exchange.
backchain withI. split. backchain oplusI. left. apply IH to H2. search.
backchain oplusI. right. apply IH to H3. search.
backchain withI. split. backchain oplusI. left. apply IH to H2. backchain exchange.
backchain oplusI. right. apply IH to H3. backchain exchange.
backchain allI. intros. backchain someI. witness x. inst H2 with n1 = x. apply IH to H3. search.
backchain allI. intros. backchain someI. witness x. inst H2 with n1 = x. apply IH to H3. backchain exchange.
backchain mu0nu0a. backchain mu0nu0b. backchain mu1nu1a. backchain mu1nu1b.
backchain mu2nu2a. backchain mu2nu2b. backchain mu3nu3a. backchain mu3nu3b.
backchain promote. backchain derelict. apply IH to H2. search.
backchain promote. backchain derelict. apply IH to H2. backchain exchange.
% An example of how to prove a theorem.
Theorem excluded-middle-multi : ts ((all x\ all y\ par (eq x y) (neq x y))::nil).
backchain allI. intros. backchain allI. intros. backchain parI. backchain neqI. intros. case H1.
backchain eqI.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Define the fixed point expressions for the natural number predicate
% and the Ackermann predicate. Also defined their De Morgan dual for
% convenient.
Define nat : (i -> pol) -> prop by
nat (mu1 (N\ x\ (oplus (eq x z) (some y\ (tensor (eq x (s y)) (N y)))))).
Define dnat : (i -> pol) -> prop by
dnat (nu1 (N\ x\ (with (neq x z) (all y\ (par (neq x (s y)) (N y)))))).
Define ack : (i -> i -> i -> pol) -> prop by
ack (mu3 (A\ x\ y\ a\ (oplus (tensor (eq x z) (eq a (s y)))
(oplus (some (p\ (tensor (eq x (s p)) (tensor (eq y z) (A p (s z) a)))))
(some p\ some q\ some b\ (tensor (eq x (s p))
(tensor (eq y (s q)) (tensor (A x q b) (A p b a))))))))).
Define dack : (i -> i -> i -> pol) -> prop by
dack (nu3 (A\ x\ y\ a\ (with (par (neq x z) (neq a (s y)))
(with (all (p\ (par (neq x (s p)) (par (neq y z) (A p (s z) a)))))
(all p\ all q\ all b\ (par (neq x (s p))
(par (neq y (s q)) (par (A x q b) (A p b a))))))))).
%%%%
%%%% Complete proof of the totality of Ackermann's function
%%%%
Theorem ack_first_induction_is_invariant:
forall N DN A DA x y, nat N -> dnat DN -> ack A -> dack DA ->
ts ((? (some (z\ tensor (N z) (all (a\ par (DA x z a) (DN a)))))) ::
DN y ::
some (a\ tensor (A x y a) (N a)) :: nil).
intros.
backchain derelict. backchain someI. witness y.
backchain tensorIx. witness (DN y :: nil).
witness (some a\ tensor (A x y a) (N a)) :: nil. split. search.
%% Tensor and splitting bureaucracy
case H1. case H2.
%Preserve: split invariant: nat and dual nat
backchain mu1nu1a.
%Preserve: split invariant: ack /\ nat and dual ack /\ dual nat
backchain allI. intros. backchain someI. witness x1.
backchain initial. case H3. case H4. case H1. case H2. search 20.
%%unfold all defs and find out the two are duals
Theorem ack_first_induction_base_case :
forall DN A N x1, ack A -> dnat DN -> nat N ->
ts (neq x1 z ::
bang (all (x\par (DN x) (some (a\tensor (A x1 x a) (N a))))) :: nil).
intros.
backchain neqI. intros. case H4. backchain promote. backchain allI. intros.
backchain parI. backchain someI. witness (s x).
backchain tensorIx. witness nil. witness (DN x :: nil). split. search.
case H1. backchain mu3I.
% Select base case of ack
backchain oplusI. left.
%% prove for ack: 0=0 and s 0 = s 0
backchain tensorI. backchain eqI. backchain eqI.
%% proving that nat x -> nat (s x) by unfolding nat (s x)
case H3. backchain mu1I. backchain oplusI. right. backchain someI. witness x.
backchain tensorIx. witness nil. witness (DN x :: nil). split. search.
backchain eqI. backchain initial. case H2. search 20.
Theorem ack_second_invariant_is_invariant :
forall DN N A DA x2 x3, ack A -> nat N -> dnat DN -> dack DA ->
ts (tensor (bang (all (x\par (DN x) (some (a\tensor (A x2 x a) (N a))))))
(all (a\par (DA (s x2) x3 a) (DN a))) ::
some (a\tensor (A (s x2) x3 a) (N a)) ::
? (some (x\tensor (N x) (all (a\ par (DA x2 x a) (DN a))))) :: nil).
intros.
backchain tensorIx.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a))))) :: nil).
witness (some (a\tensor (A (s x2) x3 a) (N a)) ::nil). split. search.
backchain initial. case H1. case H2. case H3. case H4. search 50.
backchain initial. case H1. case H2. case H3. case H4. search 50.
Theorem ack_second_induction_base:
forall N A DA DN x2 x4, ack A -> nat N -> dack DA -> dnat DN ->
ts (neq x4 z ::
par (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a))))))
(some (a\tensor (A (s x2) x4 a) (N a))) :: nil).
intros.
backchain neqI. intros. case H5. backchain parI. backchain derelict.
backchain someI. witness (s z). backchain tensorIx. witness nil.
witness (some (a\ tensor (A (s x2) z a) (N a)) :: nil). split. search.
%% one is nat
case H2. backchain mu1I. backchain oplusI. right. backchain someI. witness z.
backchain tensorI. backchain eqI. backchain mu1I. backchain oplusI. left. backchain eqI.
%% More base case: computing exists a (ack (s x2) 0 a (X) nat a) given forall a (ack x2 1 a (X) nat a)
backchain allI. intros. backchain someI. witness x.
backchain parI. backchain tensorIx. witness DA x2 (s z) x :: nil. witness DN x :: nil. split. search.
%% After introducing quantifiers and splitting: compute ack (s x2) 0 given ack x2 1
case H1. backchain mu3I. backchain oplusI. right. backchain oplusI. left. % select appropriate case of ack
backchain someI. witness x2. backchain tensorIx. witness nil.
witness (DA x2 (s z) x :: nil). split. search.
backchain eqI. backchain tensorIx. witness nil. witness DA x2 (s z) x :: nil. split. search.
backchain eqI. case H3. backchain mu3nu3a. search 10.
%% Finally, the other branch of the tensor where we prove nat x |- nat x
backchain initial. case H2. case H4. search 20.
Theorem ack_total :
forall N DN A DA, dnat DN -> ack A -> nat N -> dack DA -> forall x y,
ts ((DN x)::(DN y)::(some a\ tensor (A x y a) (N a)) ::nil).
intros. case H1.
backchain nu1Ix.
witness (y\ ? (some x \ tensor (N x) (all a\ par (DA y x a) (DN a)))).
witness (y\ bang (all x \ par (DN x) (some a\ tensor (A y x a) (N a)))).
split.
% Lemma: the chosen invariant is an invariant
backchain ack_first_induction_is_invariant with N = N, DN = DN, A = A, DA = DA.
% Induction!
intros. backchain withI. split.
% Base case in a lemma (easy but has some bureaucracy)
backchain ack_first_induction_base_case with DN = DN, A = A, N = N.
% Inductive step of main proof (we do it here since it is short)
backchain allI. intros. backchain parI. backchain neqI. intros. case H5.
backchain promote. backchain allI. intros. backchain parI.
% Time for the second induction!
backchain nu1Ix.
witness (y\ (tensor (bang (all x \ par (DN x) (some a\ tensor (A x2 x a) (N a))))
(all a\ par (DA (s x2) y a) (DN a)))).
witness (y\ (par (? (some x \ tensor (N x) (all a\ par (DA x2 x a) (DN a))))
(some a\tensor (A (s x2) y a) (N a)))).
split.
% Preserve
backchain ack_second_invariant_is_invariant with A = A, DA = DA, N = N, DN = DN.
% The second induction starts!
intros. backchain withI. split.
% Base case
backchain ack_second_induction_base with A = A, DN = DN, DA = DA, N = N.
%% Finally, the second inductive case
backchain allI. intros. backchain parI. backchain neqI. intros. case H6. backchain parI.
%% The crucial contraction and the following tensor split (corresponding to the imp-left rule in two sides)
backchain contract. backchain tensorIx.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a)))))) :: nil.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a)))))) ::
some (a\tensor (A (s x2) (s x5) a) (N a)) :: nil.
split. search.
%% Thanks to the careful splitting, we can promote here
backchain promote. backchain derelict. backchain allI. intros. backchain someI. witness x6.
%% Left hand side premise of the main imp-left rule
backchain parI. backchain tensorIx. witness DN x6 :: nil.
witness some (a\tensor (A x2 x6 a) (N a)) :: nil. split. search. case H3. backchain mu1nu1a.
backchain initial. case H2. case H4. case H3. search 20.
%% Finally, the main branch of the main imp-left rule of the second induction
backchain derelict. backchain allI. intros. backchain someI. witness x6.
backchain parI.
%% Use the tensor (i.e., imp left) to use the inductive hypothesis
backchain tensorIx. witness DN x6 :: nil.
witness DA (s x2) x5 x6 :: some (a\tensor (A (s x2) (s x5) a) (N a)) :: nil. split. search.
%% left branch of imp-left : nat x6 |- nat x6
backchain initial. case H3. search 20.
%% Finally, computing the appropriate value of ack.
%% Instanciate quantifiers (the return value is the one returned by the second call in ctx)
backchain allI. intros. backchain someI. witness x7.
%% split the two goals: the final return value x7 is a nat, and it is ack (s x2) (s x5)
backchain parI. backchain tensorIx. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil.
witness DN x7 :: nil. split. search.
%% main branch of the split: prove that x7 is the correct result
%%% unfolding the corresponding case of ack
case H2. backchain mu3I. backchain oplusI. right. backchain oplusI. right.
%%% the witnesses for the final ack unfolding
backchain someI. witness x2. backchain someI. witness x5. backchain someI. witness x6.
%%% verify the assignments for the unfolding
backchain tensorIx. witness nil. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil. split. search.
backchain eqI.
backchain tensorIx. witness nil. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil. split. search.
backchain eqI.
%%% split the two final calls to ack. Send the right premise to each branch.
backchain tensorIx.
witness DA (s x2) x5 x6 :: nil. witness DA x2 x6 x7 :: nil. split.search.
case H4. backchain mu3nu3a. search 10.
case H4. backchain mu3nu3a. search 10.
%% The other final goal: the computed vaule is nat
backchain initial. case H3. search 20.
