% 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.
%% Seq with explicit program quantification %% %% A revised external definition of seq that allows for quantification %% over lambda prolog programs. % Assume that prog has no defining clauses for now Define prog A B := false. Define lookup A (atom A) t. Define lookup A (imp B A) B. Define lookup A (and P1 P2) B := lookup A P1 B. Define lookup A (and P1 P2) B := lookup A P2 B. Define lookup A (pi P) B := exists X, lookup A (P X) B. %% We add the argument P representing the lambda prolog program so that %% we can quantify over it. Define seq P L t. Define seq P L (atom A) := member A L. Define seq P L (and A B) := seq P L A /\ seq P L B. Define seq P L (A => B) := seq P (A :: L) B. Define seq P L (pi G) := nabla x, seq P L (G x). Define seq P L (sigma G) := exists X, seq P L (G X). Define seq P L (atom A) := exists B, lookup A P B /\ seq P L B. Theorem external : forall S T, seq nil 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 %% %% This is the primary downside of this encoding: the resulting %% terms are quite large and hard to reason about. Define prog (and (pi N\ (atom (add z N N))) (pi A\ pi B\ pi C\ (imp (atom (add A B C)) (add (s A) B (s C))))). Theorem add_test : forall P, prog P -> seq P nil (atom (add (s (s z)) (s z) (s (s (s z))))). [Show Proof][Hide Proof] intros. case H1. search 10.