Chain Reasoning-constructive logic game

Stream: new members

[Kyle Yank]

image.png

[Kyle Yank]

How to solve this problem?

[Kyle Yank]

I know that I can use h2 0 h1 to solve this problem
, but I'd like to know how to show the transitivity here?

[Kyle Yank]

image.png

[Kyle Yank]

I'd like to see how to construct a transitive property
``

.

[Mark Fischer]

Ah, I just saw this. I may need some clarification to be sure what you mean. Though here is some info that might be helpful.

This is a possible solution for this level.

Assumptions:
    h1 : C → A
    h2 : A → S
Goal (C → S):
    exact λ(c: C) ↦ h2 (h1 c)

If instead of two assumptions, we had a single assumption of their conjunction instead.
h : (C → A) ∧ (A → S)

In such a situation, we can replace h1 with h.left and h2 with h.right

Assumptions:
    h : (C → A) ∧ (A → S)
Goal (C → S):
    exact λ(c: C) ↦ h.right (h.left c)

Lets say you want to create a term with the type in your picture. Here is a solution that uses this, though you'll see it's a more round-about way to get at a solution. In this case, h4 is a slight variation of what you're attempting to show this level.

Assumptions:
    h1 : C → A
    h2 : A → S
Goal (C → S):
    have h3 := and_intro h1 h2
    have h4 := λ(h : (C → A) ∧ (A → S)) (c : C) ↦ h.right (h.left c)
    exact h4 h3

[Mark Fischer]

Other ways you can write h4:

-- Desugared version (Shows both λs)
have h4 := λ(h : (C → A) ∧ (A → S)) ↦ λ(c : C) ↦ h.right (h.left c)
-- Inferred `h` and `c` from the type of `h4`
have h4 : (C → A) ∧ (A → S) → C → S := λh c ↦ h.right (h.left c)
-- Nothing implicit
have h4 : (C → A) ∧ (A → S) → C → S := λ h: (C → A) ∧ (A → S) ↦ λ c : C ↦ h.right (h.left c)