5
$\begingroup$

This doesn't work even though it is the simplest proof of an if statement that I can think of:

def f [Decidable p] (h : p) : ite p p True := ite p h trivial

It says

application type mismatch
  ite p h
argument
  h
has type
  p : Prop
but is expected to have type
  if p then p else True : Prop

I think it is possible to change the "goal" from if p then p else True to p using tactics mode, but is it possible to do it without tactics?

The reason I am asking is because I would like to know how to do things without tactics, so that I understand the fundamentals of the language better.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ ite p h trivial is a term of type Prop, while what you want is a term of type ite p p True. I believe what you want are the lemmas dif_pos and dif_neg (might be called something else in Lean 4). $\endgroup$
    – ViHdzP
    Commented Jul 2, 2022 at 19:20
  • 3
    $\begingroup$ @ViHdzP @tydeu "ite .. is a term of type Prop" is not true, the type of ite is whatever the type of both of its branches is. Which means that this ite application is not typeable as the two branches have different types, but they are proofs, not Props. Because of proof irrelevance, it never makes sense to apply ite to proofs of course. $\endgroup$
    – Sebastian Ullrich
    Commented Jul 3, 2022 at 7:51
  • $\begingroup$ Sebastian is correct. I have updated my answer to be more accurate about the types. $\endgroup$
    – tydeu
    Commented Jul 8, 2022 at 5:48
  • $\begingroup$ You can use ▸ (aka Eq.ndrec) to make the term well typed: example (p : Prop) [Decidable p] : ite p p True := dite p (fun h => if_pos h ▸ h) (fun h => if_neg h ▸ trivial) $\endgroup$
    – François G. Dorais
    Commented Jul 8, 2022 at 20:32

1 Answer 1

Reset to default
4
$\begingroup$

Instead of using ite to branch on p you want to use match on the Decidable p instance like so:

def f [d : Decidable p] (h : p) : ite p p True :=
  match d with
  | isTrue _ => h 
  | isFalse _ => trivial

As Sebastian notes in his comment, ite p h trivial is an ill-typed term (h is of type p and True is of type Prop. And as ViHdzP notes, what we want is to produce a term of type ite p p True.

To see why are the above solution works, consider the parallel proof with tactics:

def f' [d : Decidable p] (h : p) : ite p p True := by
  unfold ite -- ⊢ Decidable.casesOn d (fun x => True) fun x => p
  cases d with
  | isTrue _ => -- ⊢ Decidable.casesOn (isTrue h✝) (fun x => True) fun x => p
    dsimp -- ⊢ p
    exact h -- Goals accomplished 🎉
  | isFalse _ => -- ⊢ Decidable.casesOn (isFalse h✝) (fun x => True) fun x => p
    dsimp -- Goals accomplished 🎉 -- reduces to True and thus closes the goal
Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.