quantification in iffs

Stream: new members

[Yakov Pechersky]

A question on how to write implications. I have the following lemma:

import data.buffer.parser.basic

namespace parser

open parse_result
variables {β α : Type} {cb : char_buffer} {n' n : ℕ} {a' a : α} {b : β} {c : char} (hn : n < buffer.size cb)
include hn

lemma any_char_eq_done : any_char cb n = done n' c ↔ n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c :=
by simp [any_char, hn, eq_comm]

end parser

[Yakov Pechersky]

How can I rephrase it to put the hn : n < buffer.size cb on the right side of the \iff? I only need it to construct the cb.read ⟨n, hn⟩. Is that even possible?

[Yakov Pechersky]

These proofs would suggest that, yes:

lemma any_char_eq_done_imp_lt (h : any_char cb n = done n' c) : n < cb.size :=
begin
  contrapose! h,
  simp [any_char, h]
end

lemma any_char_eq_done_imp (h : any_char cb n = done n' c) :
  n + 1 = n' ∧ cb.read ⟨n, any_char_eq_done_imp_lt h⟩ = c :=
begin
  simp [any_char] at h,
  split_ifs at h with hn,
  { assumption },
  { contradiction }
end

lemma imp_any_char_eq_done (hn : n + 1 = n') (hle : n < cb.size) (h : cb.read ⟨n, hle⟩ = c) :
  any_char cb n = done n' c :=
by simp [any_char, hn, hle, h]

[Yakov Pechersky]

Since the LHS implies the constraint for the RHS

[Floris van Doorn]

You could write

any_char cb n = done n' c ↔ ∃ (hn : n < buffer.size cb), n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c