syntax to negate a propositional hypothesis?

Stream: new members

[Daniel Windham]

Dumb question - given a hypothesis such as h : 1 + 1 = 3, how do I construct its negation ¬ h?

I'm getting an error

application type mismatch
 ¬h
argument
 h
has type
 1 + 1 = 3 : Prop
but is expected to have type
 Prop : Type

Here's the full code example:

theorem demo (h: 1 + 1 = 3) : false := by
  have h2: ¬ h := by
    sorry
  contradiction

Related vocabulary question - in informal conversation, is there a precise way to say that the type of the type of h is Prop? I wrote "propositional hypothesis" in my topic title but I don't know if that means what I want.

Thanks!

[Jireh Loreaux]

The type of h is not Prop. The type of h is 1 + 1 = 3, that's exactly what h : 1 + 1 = 3 means. Here h is proof that 1 + 1 = 3.

[Jireh Loreaux]

That's why you can't write ¬ h, because ¬ : Prop → Prop. You can't take the negation of a proof.

[Daniel Windham]

@Jireh Loreaux it sounds like I'm stuck on something deeper then. I am trying to construct a proof by contradiction. If I write have h2: ¬ (1 + 1 = 3) in my original example, the proof by contradiction completes. I'd rather write h2 in terms of h1 because it will be more concise. In my real example, h1 is a lot longer to write out. Does Lean provide a way to write h2 in terms of h1?

[Richard Copley]

You could do something like the following, but it's less useful than you might think.

def TypeOf {α : Sort*} (x : α) := α

theorem demo (h: 1 + 1 = 3) : False := by
  have h2: ¬ (TypeOf h) := by
    unfold TypeOf
    -- ⊢ ¬1 + 1 = 3
    sorry
  contradiction

It's easier to use the contrapose tactic:

theorem demo (h: 1 + 1 = 3) : False := by
  contrapose h
  -- ⊢ ¬1 + 1 = 3
  sorry

[Daniel Windham]

Thanks @Richard Copley , that's what I was looking for.

Agreed that contrapose usually makes more sense. However, I don't have contrapose right now because I'm working in the std library. (Perhaps contrapose belongs in std, I haven't gone and asked anyone yet...)

[Patrick Massot]

contrapose is a tiny tactic that could very easily move to std or your own code. The more complicated bit is contrapose!.

[Richard Copley]

Or there's this:

theorem demo (h: 1 + 1 = 3) : False := by
  revert h
  -- 1 + 1 = 3 → False
  sorry

[Patrick Massot]

Hopefully you can simply drop

namespace Mathlib.Tactic.Contrapose

lemma mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) := fun h hp ↦ by_contra (fun h' ↦ h h' hp)

/--
Transforms the goal into its contrapositive.
* `contrapose`     turns a goal `P → Q` into `¬ Q → ¬ P`
* `contrapose h`   first reverts the local assumption `h`, and then uses `contrapose` and `intro h`
* `contrapose h with new_h` uses the name `new_h` for the introduced hypothesis
-/
syntax (name := contrapose) "contrapose" (ppSpace colGt ident (" with " ident)?)? : tactic
macro_rules
  | `(tactic| contrapose) => `(tactic| (refine mtr ?_))
  | `(tactic| contrapose $e) => `(tactic| (revert $e:ident; contrapose; intro $e:ident))
  | `(tactic| contrapose $e with $e') => `(tactic| (revert $e:ident; contrapose; intro $e':ident))

into your current file.

[Jireh Loreaux]

Also, since you're in Std, you can just use omega to close this goal:

import Std

theorem demo (h : 1 + 1 = 3) : false := by omega

[Daniel Windham]

@Patrick Massot it looks like there are a few more missing definitions in std:

lemma errors with unexpected identifier; expected command. I assume this is an alias for theorem defined outside of std. I replaced it with theorem, at which point I hit the next error:

by_contra errors with unknown identifier 'by_contra' . Is this definition easy to pull from Mathlib? I'm not sure what to make of this, since I can use by_contra as a tactic within a proof.

[Eric Wieser]

Richard Copley said:

You could do something like the following, but it's less useful than you might think.

def TypeOf {α : Sort*} (x : α) := α

This is builtin to Lean as type_of% x, which unfolds immediately

[Richard Copley]

Daniel Windham said:

I'm not sure what to make of this, since I can use by_contra as a tactic within a proof.

The tactic by_contra is in Std.Tactic.Basic, but the ("term-mode") function by_contra is in Mathlib.Logic.Basic.

[Patrick Massot]

theorem mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) :=
fun h hp ↦  Decidable.byCases (dec := Classical.propDecidable _) id fun nq ↦ (h nq hp).elim

[Kyle Miller]

@Jireh Loreaux Or there's theorem demo (h : 1 + 1 = 3) : false := by cases h since there are no free variables (it analyzes the constructors).

[Daniel Windham]

Patrick Massot said:

theorem mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) :=
fun h hp ↦  Decidable.byCases (dec := Classical.propDecidable _) id fun nq ↦ (h nq hp).elim

Thanks @Patrick Massot that works now.

[Jireh Loreaux]

@Kyle Miller what fun is a mallet when you have a sledgehammer? :wink: (joking of course)

[Matt Diamond]

@Daniel Windham maybe I'm off base but it sounds like you're really just trying to do this:

def P : Prop := [very long and complicated proposition]

theorem demo (h1 : P) : false := by
  have h2: ¬ P := by
    sorry
  contradiction

There's no need for type_of% or anything like that. The key to writing h2 in terms of h1 is to abstract out the common element into its own definition.

[Daniel Windham]

@Matt Diamond thanks, that's a good trick. That's not quite my situation here, since the complicated proposition is the result of unfolding (and simplifying) subexpressions in the theorem's hypothesis. Is there a tactic to abstract out a subexpression from an existing goal or hypothesis in the proof state? I'd like to do something like this:

theorem demo ... := by
    simp [...]
    intro h
    let len := fun (x: AssocList α β) => List.length (AssocList.toList x) -- define the subexpression
    rw [len] -- replace the subexpression in the goal with `len`
    rw [len] at h -- replace the subexpression in `h` with `len`

[Matt Diamond]

maybe the set tactic? it's like let but it replaces expressions with the newly defined variable where it can

[Daniel Windham]

Ah perfect, set is what I was looking for. (Though it's another tactic that's not in std lib, hmm...) Thanks @Matt Diamond!

[Matt Diamond]

no problem!

[Daniel Windham]

Here's a way to do this without set. This is what set does under the hood:

theorem demo (h: 1 + 1 = 3) : 1 + 1 + 1 + 1 + 1 = 6 := by
  let z := 1 + 1
  let hh: z = 1 + 1 := by rfl -- construct an equality corresponding to the new definition
  rw [← hh]
  rw [← hh] at h