(* Today we discuss AND and OR. *)
(* We can check out their definitions. *)
Print and.
Print or.
(* Notice that they're located in the Logic library. *)
Locate and.
Locate or.
(* AND and OR are fundamental enough that hints about them appear in the core database. *)
Print Hint and.
Print Hint or.
(* First we try proving a conjunction. *)
Goal (3 <= 5) /\ True.
Proof.
(* To prove a conjunction, we must prove both subgoals.
We'll prove each of the resulting subgoals using auto, since there's nothing
new about them. We separate the steps, so we can inspect the
intermediat proof. *)
apply conj.
Show Proof.
auto.
auto.
Qed.
(* We can also use a special purpose tactic, split, to prove the same subgoal. *)
Goal (3 <= 5) /\ True.
Proof.
(* split is a slightly general tactic that can be used to break up goals into there
components. It works for conjunctions, but also for other inductive definitions
with a unique constructor.
We'll prove each of the resulting subgoals using auto, since there's nothing
new about them. *)
(info split); info auto.
Qed.
(* It turns out we can prove the whole thing using auto, since apply conj is in
the core database and the subgoals are easily proved using auto. If the
subgoals could not be proved, auto would fail. *)
Goal (3 <= 5) /\ True.
Proof.
auto.
Qed.
(* Now we try to prove a disjunction using some basic tactics. *)
Goal (2 <= 5) \/ False.
Proof.
(* Clearly we want to prove the left side of the disjuction.
We assert our intention using or_introl. *)
apply or_introl.
Show Proof.
(* Here we see that the first argument to or_introl is the type of the goal it is _not_
proving. *)
auto.
Qed.
(* We'll prove this goal again, using slightly more general tactics. *)
Goal (2 <= 5) \/ False.
Proof.
(* The tactic, left, is general, like split. It works for OR, but also for other
inductive definitions with two constructors. left chooses the first constructor.
The right tactic will always choose the second constructor. *)
(info left); auto.
Qed.
(* We can actually prove the whole thing using auto, since apply or_introl is in
the core hint database and the two subgoals are proved with auto. *)
Goal (2 <= 5) \/ False.
Proof.
auto.
Qed.
(* AND has induction schemes in all three sorts; another exception to the Prop rule. *)
Print and_ind.
Print and_rect.
Print and_rec.
(* OR does not have three induction schemes; it's normal. *)
Print or_ind.
(* Let's check the type of conj. *)
Check conj.
(* Notice that it has four arguments, and our pattern matching uses only two. Why? *)
(* Let's pretend that conj is overloaded. It's a function that builds an expression and
it's a label. I don't know if this is true, but it makes the typechecking work so far. *)
(* Some of the arguments are implicit, which means they can be inferred from subsequent
arguments. *)
Print Implicit conj.
(* We are prohibited from supplying A and B to conj, because they're implicit. *)
Check (conj I (le_n O)).
(* Or we can use @. It's a note to Coq that says I'm going to supply all
arguments, even if some are implicit. *)
Check (
match @conj True (O <= O) I (le_n O) return True with
| conj a b => a
end).
(* We can leave the implicit args out. *)
Check (
match conj I (le_n O) return True with
| conj a b => a
end).
(* What does structural induction on AND really mean? AND is not recursively defined. *)
(* We take a break here and discuss well-founded induction. In particular, we construct
the maximal induction principle. *)
(* Our first hint, we can hold A and B constant throughout. *)
(* forall (A B : Prop), ... *)
(* What's the type of P, the thing that we're trying to prove. *)
(* forall (A B : Prop) (P : forall (Z : A /\ B), Prop), .... *)
(* OK, how many constructors do we have? *)
(* Just one, so there's only one principle premise. *)
(* forall (A B : Prop) (P : forall (Z : A /\ B), Prop),
(forall (a : A) (b : B), P (conj a b)) -> forall (Z : A /\ B), P Z *)
(* OK, let's prove it. *)
Goal forall (A B : Prop) (P : forall (Z : A /\ B), Prop),
(forall (a : A) (b : B), P (conj a b)) -> forall (Z : A /\ B), P Z.
intros.
(* We solve the rest explicitly. It's unnecessary to write a fixpoint.
But it's necessary to include an as annotation to make sure that
the type varies appropriately. *)
refine (match Z as Z0 return P Z0 with
| conj a b => _ : P (conj a b)
end).
auto.
Qed.
(* We use Coq to check that our maximal induction principle is correct. *)
Scheme and_rect' := Induction for and Sort Type.
Print and_rect'.
(* AND is in Prop, so the induction principle we get by default is the minimal one. *)
(* Note that type annotations are unnecessary. *)
Print and_rect.
(* We prove modus ponens. *)
Goal forall (A B : Prop), A /\ (A -> B) -> B.
intros.
(* Note that auto is unsuccesful. *)
auto.
(* We do induction on the conjunction. *)
induction H.
auto.
Qed.
(* We can prove the same goal differently. *)
Goal forall (A B : Prop), A /\ (A -> B) -> B.
intros.
(* We can apply H, relying on the apply to match H with it's one constructor and
to select the appropriate argument, the second. *)
apply H.
Show Proof.
(* We can apply H one more time, again relying on the apply tactic to do its own
deconstructing. *)
apply H.
Show Proof.
Qed.
(* Note that we can rely on the apply tactic to its own destructuring only
when the inductive type has only one constructor. The same approach
with the following inductive type will fail. *)
Inductive and2 (A : Prop) (B : Prop) : Prop :=
| conj1 : forall (a : A) (b : B), and2 A B
| conj2 : forall (a : A) (b : B), and2 A B
.
Goal forall (A B : Prop), and2 A (A -> B) -> B.
intros.
(* applying H at this point will fail. However, we can proceed by induction. *)
induction H; auto.
Qed.