Prove some simple laws

Using Coq
1

Hello! I’m new in Coq and I can’t understand how to prove such laws( Can someone help me with some please?
(A → B) → (A → C) → (B → C → D) → (A → D);
(A → A → B) → (A → B);
(A → B) → (A → A → B);
(A → C) → A → B → C;
(A → B) → (B → C) → A → C.

2

Think of it as a functional programming task. In the first goal, you have functions f1 : A -> B, f2 : A -> C, f3 : B -> C -> D and an element a : A. How can you give an element of D? It turns out that you only need the application f1 a. You can write this in Coq like this:

Lemma L1 (A B C D : Prop) :
  (A -> B) -> (B -> C) -> (B -> C -> D) -> (A -> B).
Proof.
  exact (fun (f1 : A -> B) (f2 : B -> C) (f3 : B -> C -> D) (a : A) => f1 a).
Qed.

Lemma L2 (A B : Prop) :
  (A -> A -> B) -> (A -> B).
Proof.
  exact (fun (f1 : A -> A -> B) (a : A) => f1 a a).
Qed.

I leave the rest of the lemmas as an exercise for you. Note that the tactic tauto can solve all these goals.

You can also use tactics. Instead of using fun, you can use intros:

Lemma L1' (A B C D : Prop) :
  (A -> B) -> (B -> C) -> (B -> C -> D) -> (A -> B).
Proof.
  intros f1 f2 f3 a.
  exact (f1 a).
Qed.
1 Like
3

Thank you! But I still don’t understand how to solve next lemmas(( can you help me again please? I really tried

4

With the approach @mwuttke97 suggested, each implication is a function with the given type. For example, A -> B is a function from type A to type B. Then proving a lemma is writing a function taking arguments of the correct types and resulting in the correct type. If you try typing the functions from mwuttke97’s answer, you will see that the types match the lemma being proven. With this view, you can use your intuition from functional programming.

An alternative view is to look at proofs from logic. For example, a proof for your first lemma would be:

Lemma L1 : forall (A B C D : Prop),
    (A -> B) -> (A -> C) -> (B -> C -> D) -> (A -> D).
Proof.
  intros A B C D AtoB AtoC BtoCtoD isA.
  apply BtoCtoD.
  - apply AtoB. apply isA.
  - apply AtoC. apply isA.
Qed.

The intros tactic lets you introduce variables (A, B, C, and D) and hypotheses (AtoB, AtoC, BtoCtoD, and isA). The apply tactic lets you use an implication to prove a goal when the head of the implication matches the goal, then requires you to prove the antecedents of the implication.

Either approach will work for proving all the lemmas you are looking at. Which approach you want to take depends on whether you are more comfortable with logic or functional programming. I suggest you try working out the rest of the lemmas yourself for practice using Coq. If you intend to use Coq, you will need to learn to handle lemmas like this.

Edit: I hit a key which posted this before I was ready.