PRFA.review6

Reviewing session 6

SELF-EVALUATION

1. Give the induction principle for list *together* with its proof term. 2. Give the induction principle for Acc. 3. Which of the following proof scripts fail? For those who do not fail, what is the goal (assumptions and conclusions) after executing them?

(Ignore the try they are here to allow Coq to build the HTML without telling you which goals fail or not.)

Inductive list A :=
| nil
| cons (a : A) (l : list A).

Inductive Acc {A} (R : A → A → Prop) : A → Prop :=
| Acc_intro x : (∀ y, R y x → Acc R y ) → Acc R x.

Ltac tac :=
  match goal with
  | |- ?A ∨ ?B ⇒ left
  | h : ?A |- ?A ⇒ apply h
  end.

Goal ∀ P Q , P → P ∨ Q.
Proof.
  try intros P Q hP.
  try tac.
  (* HERE *)
Abort.

Goal True ∨ (False → False ).
Proof.
  try constructor ; intro x.
  (* HERE *)
Abort.

Goal True ∨ (False → False ).
Proof.
  try constructor. try intro x.
  (* HERE *)
Abort.