its a rw bug?

Stream: new members

[lorã]

ok, maybe im posting to much, but look at that:

theorem Λsub_refl [DecidableEq α] : ∀ (M : Λ α), M is a subterm of M := by {
  intros M
  unfold Λ.sub
  cases M
  case var x =>
    simp [Bag.singleton, Bag.has]
  case app N M =>
    simp [Bag.has]
    have := sing_one (N.app M)
    rw [this]
}

the last line had fail with this:

this : (Bag.singleton (N.app M)).count (N.app M) = 1
⊢ 0 < (N.sub + M.sub + Bag.singleton (N.app M)).count (N.app M)

[lorã]

Here's the whole code if u wanna try it:

-- I want to provide an interface with only proposition uses. (no computational worries here.)
-- The interface will be:
-- how much times are you there?
-- are u there? (are u 0 times there?)

universe u

structure Bag (α : Type u) where
  count : α → Nat

def Bag.has (b : Bag α) (a : α) := b.count a > 0

def Bag.add (b₁ b₂ : Bag α) :=
  Bag.mk (fun a => b₁.count a + b₂.count a)

def Bag.singleton [DecidableEq α] (a : α) : Bag α :=
  Bag.mk (fun a' => if a = a' then 1 else 0)

def Bag.sub (b₁ b₂ : Bag α) : Prop :=
  ∀ (x : α), b₁.count x ≤ b₂.count x

instance : Add (Bag α) where
  add := Bag.add


notation a " ∈ " b => Bag.has b a
notation:80 a:80 " ∪ " b:80 => Bag.union a b
notation a " ∩ " b => Bag.intersection a b
notation a " ⊆ " b => Bag.sub a b


theorem sing_one [DecidableEq α] : ∀ (a : α), (Bag.singleton a).count a = 1 := by
  intro x
  unfold Bag.singleton
  simp [Bag.count]

inductive Λ (V : Type u) where
  | var (_ : V)
  | app (M N : Λ V)
  | abs (_ : V) (M : Λ V)
deriving DecidableEq open Λ


def Λ.sub [DecidableEq α] (expr : Λ α) : Bag (Λ α) :=
  let s := Bag.singleton expr
  match expr with
  | var _   => s
  | app M N => M.sub + N.sub + s
  | abs _ M => M.sub + s

notation L " is " " a " " subterm " " of " M => L ∈ Λ.sub M


theorem Λsub_refl [DecidableEq α] : ∀ (M : Λ α), M is a subterm of M := by {
  intros M
  unfold Λ.sub
  cases M
  case var x =>
    simp [Bag.singleton, Bag.has]
  case app N M =>
    simp [Bag.has]
    have := sing_one (N.app M)
    rw [this]



}

[Kevin Buzzard]

ok, maybe im posting to much, but look at that:

Just to emphasize: there is no limit on the number of basic questions you can ask in #new members , especially if you are asking them because you're motivated to learn!

[Kevin Buzzard]

The error message which you're getting

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  (Bag.singleton (N.app M)).count (N.app M)
α : Type u_1
inst✝ : DecidableEq α
N M : Λ α
this : (Bag.singleton (N.app M)).count (N.app M) = 1
⊢ 0 < (N.sub + M.sub + Bag.singleton (N.app M)).count (N.app M)

looks correct to me. There is no (Bag.singleton (N.app M)).count (N.app M) in your goal -- there is something which is very very close to that, but it's not x.count y, it's (a+b+x).count y, so the exact LHS of this is missing and this is why the rewrite fails.