likely stupid question here, I'm sure, but I have been trying fruitlessly with little success to figure this problem out. Here is a toy example. Suppose we have this.
def f (x : Nat) := match x with
| 0 => 0
| n + 1 =>
have : x = n + 1 := by sorry
3
How do we prove that statement, that x = n + 1? This seems like it should be obvious. The full example where this comes up is of course more involved -- if anyone thinks I can do it easily another way, please be my guest; I am trying to prove soundness for a subset of propositional logic with just # and ->.
inductive Expr where
| bot : Expr
| var (s : String) : Expr
| imp (p q : Expr) : Expr
infixl:80 " ==> " => Expr.imp
notation "⊥" => Expr.bot
inductive TruthVal where
| T : TruthVal
| F : TruthVal
def eval (e : Expr) (env : String -> TruthVal) : TruthVal := match e with
| ⊥ => TruthVal.F
| Expr.var s => env s
| p ==> q => match eval p env with
| TruthVal.T => eval q env
| TruthVal.F => TruthVal.T
def Set u := u -> Prop
def Set.union (u1 : Set u) (u2 : Set u) : Set u := fun u' => u1 u' ∨ u2 u'
def Set.add (u1 : Set u) (u2 : u) : Set u := fun u' => u1 u' ∨ u' = u2
def Set.subset (s S : Set u) : Prop := ∀ u', s u' -> S u'
def Set.unionSubset (eq : Set.union x y = z) : Set.subset x z :=
fun u g =>
let hp : x u := by
subst eq
exact g
let or : x u ∨ y u := Or.intro_left (y u) hp
by
subst eq
rw [union]
exact or
inductive Proof : Set Expr -> Expr -> Type u where
| premise : premises q -> Proof premises q
| doubleNegation : Proof premises (Expr.imp (Expr.imp p Expr.bot) Expr.bot) -> Proof premises p
| direct : Proof (Set.add premises p) q -> Proof premises (Expr.imp p q)
| modusPonens
(proof1 : Proof prems1 (Expr.imp p q))
(proof2 : Proof prems2 p)
(eq_proof : Set.union prems1 prems2 = premises) : Proof premises q
def entails (Γ : Set Expr) (φ : Expr) : Prop :=
∀ model : String -> TruthVal,
(∀ premise : Expr, Γ premise -> eval premise model = TruthVal.T) ->
eval φ model = TruthVal.T
infixl:65 " ⊢ " => Proof
infixl:65 " ⊨ " => entails
def Proof.hypotheses : prems ⊢ concl -> Set Expr := fun _ => prems
def Proof.conclusion : prems ⊢ concl -> Expr := fun _ => concl
theorem Proof.soundness : Γ ⊢ φ -> Γ ⊨ φ :=
fun (p : Γ ⊢ φ)
(model : String -> TruthVal)
(premisesHold : ∀ premise : Expr, Γ premise -> eval premise model = TruthVal.T)
=> match p with
| premise proof => premisesHold φ proof
| doubleNegation proof =>
let ih : Γ ⊨ φ ==> ⊥ ==> ⊥ := proof.soundness
let result : TruthVal.T = eval φ model := calc
TruthVal.T = eval (φ ==> ⊥ ==> ⊥) model := Eq.symm (ih model premisesHold)
_ = eval φ model :=
by
repeat rw [eval]
cases (eval φ model)
repeat simp
Eq.symm result
| direct subproof =>
let ih := subproof.soundness
by
rename_i assumption conclusion
rw [eval]
let allPremsHoldIfAssumptionTrue :
eval assumption model = TruthVal.T -> ∀ premise : Expr, (Set.add Γ assumption) premise -> eval premise model = TruthVal.T
:= fun hyp premise =>
by
rw [Set.add]
intro or
cases or with
| inl h => have g := premisesHold premise h; exact g
| inr h => rw [h]; exact hyp
cases (eval assumption model) with
| F => simp
| T =>
simp
exact ih model (allPremsHoldIfAssumptionTrue sorry)
| modusPonens proof1 proof2 eq => sorry
In particular, I am looking for something to deal with the first sorry -- that is, a term of eval assumption model = TruthVal.T, which seems like it should be obvious to get.
Many thanks in advance.
