help with curry howard correspondence

Stream: general

[Kind Bubble]

Can someone help me complete my puzzle? I'm trying to jumpstart my Curry-Howard correspondence by proving this theorem

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : Π(_ : p),⊛-> p := sorry

[Mario Carneiro]

I think there is likely a precedence issue here

[Kind Bubble]

Mario Carneiro said:

I think there is likely a precedence issue here

What's that mean?

[Mario Carneiro]

you should put parentheses in to clarify whether you mean (Π(_ : p),⊛) -> p or Π(_ : p), (⊛ -> p)

[Mario Carneiro]

With the parentheses as you have placed them, the statement is false

[Kind Bubble]

Mario Carneiro said:

you should put parentheses in to clarify whether you mean (Π(_ : p),⊛) -> p or Π(_ : p), (⊛ -> p)

Ok I made edits here it is now:

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : (Π(_ : p),⊛) -> p := sorry

[Mario Carneiro]

because Π(_ : p),⊛ is always inhabited, by the constant function (x:p) ↦ *, but p is only inhabited sometimes

[Mario Carneiro]

so if we consider p = false for example then the sorry is false

[Kind Bubble]

Π(_ : p),⊛ could be ... oh! I wanted dependent sum!

Ok ok...

[Mario Carneiro]

that would be Sigma fun (X : A) => F

[Kind Bubble]

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : (Σ(_ : p ),⊛) -> p := sorry
def and_this_one : p ->  (Σ(_ : p ),⊛) := sorry

[Mario Carneiro]

fun hp => hp.1 and fun hp => \<hp, *\> respectively

[Kind Bubble]

poifect thanks a million. oh and one more:

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
def uniq : Π(x :⊛ ),Π(y :⊛),(Σ(p:x=y),⊛) := sorry

[Kind Bubble]

(deleted)