% We do not use any internal definitions since we are going to use an % external representation lambda prolog.
Click on a command or tactic to see a detailed view of its use.
%% Comparison between internal and external definition of seq % prog holds the object level program which is addition in this case Define prog (nat z) t. Define prog (nat (s N)) (atom (nat N)). Define prog (add z N N) t. Define prog (add (s A) B (s C)) (atom (add A B C)). Define seq L t. Define seq L (atom A) := member A L. Define seq L (and A B) := seq L A /\ seq L B. Define seq L (A => B) := seq (A :: L) B. Define seq L (pi G) := nabla x, seq L (G x). Define seq L (sigma G) := exists X, seq L (G X). Define seq L (atom A) := exists B, prog A B /\ seq L B. Theorem external : forall S T, seq nil (pi x\ p x S => pi y\ p y T => atom (p x T)) -> S = T. [Show Proof][Hide Proof] intros. case H1. case H2. case H3. case H4. case H5. case H6. case H7. search. case H8. case H6. Theorem internal : forall S T, {pi x\ p x S => pi y\ p y T => p x T} -> S = T. [Show Proof][Hide Proof] intros. case H1. case H2. case H3. search. case H4. %% An external version of add.mod/thm %% %% The primary difference (besides the extra syntax of "atom") is that %% for (seq nil P) we have to consider both (member P nil) and %% (prog P B, seq nil B). Then we have to do case analysis on (prog P B) %% to unfold the body of P. In the internal version, all of this is %% contained in one case analysis. Theorem add_base : forall N, seq nil (atom (nat N)) -> seq nil (atom (add N z N)). [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3. search. Theorem add_step : forall A B C, seq nil (atom (add A B C)) -> seq nil (atom (add A (s B) (s C))). [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3. search. Theorem add_comm : forall A B C, seq nil (atom (nat B)) -> seq nil (atom (add A B C)) -> seq nil (atom (add B A C)). [Show Proof][Hide Proof] induction on 2. intros. case H2. case H3. case H3. apply add_base to H1. search. apply IH to H1 H4. apply add_step to H5. search. %% A benefit of the external definition of seq is that it allows us to prove %% meta-theoremas about lambda prolog. Since these proofs require more than %% just structural induction on seq, we define seq/3 which is annotated %% with an explicit measure. Define seq N L t. Define seq N L (atom A) := member A L. Define seq (s N) L (and A B) := seq N L A /\ seq N L B. Define seq (s N) L (A => B) := seq N (A :: L) B. Define seq (s N) L (pi G) := nabla x, seq N L (G x). Define seq (s N) L (sigma G) := exists X, seq N L (G X). Define seq (s N) L (atom A) := exists B, prog A B /\ seq N L B. %% We show that seq/3 is no more powerful than seq/2 Theorem seq3_seq2 : forall N L G, seq N L G -> seq L G. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. search. apply IH to H2. apply IH to H3. search. apply IH to H2. search. apply IH to H2. search. apply IH to H2. search. apply IH to H3. search. %% Not only do permutations not effect provability, but they also %% preserve proof height. Theorem seq_subset : forall L1 L2 G N, seq N L1 G -> (forall X, member X L1 -> member X L2) -> seq N L2 G. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply H2 to H3. search. apply IH to H3 H2. apply IH to H4 H2. search. assert forall X, member X (A :: L1) -> member X (A :: L2). intros. case H4. search. apply H2 to H5. search. apply IH to H3 H4. search. apply IH to H3 H2. search. apply IH to H3 H2. search. apply IH to H4 H2. search. %% The main result is that seq/3 admits a cut property. The proof is on %% the height of one of the derivations, but note that the induction %% cannot be structural since we must at one point permute the context %% before the inductive hypothesis can be applied. Define nat z. Define nat (s X) := nat X. Theorem seq3_cut : forall K L G N M, nat N -> seq N (K :: L) G -> seq M L (atom K) -> seq L G. [Show Proof][Hide Proof] induction on 1. intros. case H2. search. case H4. apply seq3_seq2 to H3. search. % Key case: G=K search. case H1. apply IH to H6 H4 H3. apply IH to H6 H5 H3. search. assert forall X, member X (A :: K :: L) -> member X (K :: A :: L). intros. case H5. search. case H6. search. search. apply seq_subset to H4 H5. assert forall X, member X L -> member X (A :: L). intros. search. apply seq_subset to H3 H7. case H1. apply IH to H9 H6 H8. search. case H1. apply IH to H5 H4 H3. search. case H1. apply IH to H5 H4 H3. search. case H1. apply IH to H6 H5 H3. search. %% Another important result is that nabla variables can be treated as %% universally quantified inside of seq. That is, we can always %% instantiate them. Furthermore, this instantiation does not increase %% the proof height. Theorem member_inst : forall L A T, nabla x, member (A x) (L x) -> member (A T) (L T). [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2 with T = T. search. Theorem prog_inst : forall A B T, nabla x, prog (A x) (B x) -> prog (A T) (B T). [Show Proof][Hide Proof] intros. case H1. search. search. search. search. Theorem seq_inst : forall N L G T, nabla x, seq N (L x) (G x) -> seq N (L T) (G T). [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply member_inst to H2 with T = T. search. apply IH to H2 with T = T. apply IH to H3 with T = T. search. apply IH to H2 with T = T. search. apply IH to H2 with T = T. search. apply IH to H2 with T = T. search. apply prog_inst to H2 with T = T. apply IH to H3 with T = T. search.