import MyNat.Definition
namespace MyNat
open MyNat

Advanced Proposition world

Level 1: the constructor tactic.

The logical symbol ∧ means "and". If P and Q are propositions, then P ∧ Q is the proposition "P and Q". If your goal is P ∧ Q then you can make progress with the constructor tactic., which turns one goal ⊢ P ∧ Q into two goals, namely ⊢ P and ⊢ Q. In the level below, after a constructor, you can finish off the two new sub-goals with the exact tactic since both p and q provide exactly what we need. You could also use the assumption tactic.

Lemma

If P and Q are true, then P ∧ Q is true.

example: ∀ (P Q : Prop), P → Q → P ∧ Q
example (
P: Prop
P 
Q: Prop
Q : 
Prop: Type
Prop) (
p: P
p : 
P: Prop
P) (
q: Q
q : 
Q: Prop
Q) : 
P: Prop
P ∧ 
Q: Prop
Q := 
P, Q: Prop
p: P
q: Q
P ∧ Q

  
P, Q: Prop
p: P
q: Q
left
P
P, Q: Prop
p: P
q: Q
Q

  
P, Q: Prop
p: P
q: Q
right
Q

  
Goals accomplished! 🐙

Next up Level 2