boolean - 如何解决 ∀ a : bool → bool, ∀ b : bool, a (a (ab)) = ab in Lean

Question

我试图解决这个问题，但不能，有什么帮助吗？到目前为止我的解决方案：

example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=
begin
     assume a b,
     cases a:b,
     cases b,
     cases a,
     have c : tt ≠ ff,
     contradiction,
     sorry,
end

Answer 1

使用你的战术风格：

example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=
begin
  assume a b,
  -- split reasoning into b as ff or tt
  cases hb : b,
  { -- in this case, all b is now ff
    -- so let's split what (a ff) is into ff and tt
    -- since we have two (a ff) expressions in our goal
    cases hf : a ff,
    { -- this case is where (a ff) = ff,
      -- so we use it directly twice
      exact hf.symm ▸ hf },
    { -- in this case, (a ff) = tt, so now we have
      -- the expression (a tt) in our goal
      -- we split it into the cases ff and tt
      cases ht : a tt,
      { -- in this case, we already have the goal, use it
        exact hf },
      { -- in this case, we already have the goal, use it
        exact ht } } },
  { -- in this case, all b is now ff
    -- so let's split what (a tt) is into ff and tt
    -- since we have two (a tt) expressions in our goal
    cases ht : a tt,
    { -- in this case, (a tt) = ff, so now we have
      -- the expression (a ff) in our goal
      -- we split it into the cases ff and tt
      cases hf : a ff,
      { -- in this case, we already have the goal, use it
        exact hf },
      { -- in this case, we already have the goal, use it
         exact ht } },
    { -- this case is where (a tt) = tt,
      -- so we use it directly twice
      exact ht.symm ▸ ht } },
end

在 case-bash 变体中，仍然没有策略：

example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=
begin
  intros a b,
  -- split reasoning into b as ff or tt
  cases hb : b;
  -- and for all cases, split reasoning of the (a ff) expression
  cases hf : a ff;
  -- and for all cases, split reasoning of the (a tt) expression
  cases ht : a tt,
  -- now deal with all cases
  { exact hf.symm ▸ hf },
  { exact hf.symm ▸ hf },
  { exact hf },
  { exact ht },
  { exact hf.symm ▸ hf },
  { exact ht.symm ▸ ht },
  { exact hf.symm ▸ ht },
  { exact ht.symm ▸ ht },
end

最后，使用简单的策略：

example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=
begin
  intros a b,
  -- split reasoning into b as ff or tt
  cases hb : b;
  -- and for all cases, split reasoning of the (a ff) expression
  cases hf : a ff;
  -- and for all cases, split reasoning of the (a tt) expression
  cases ht : a tt;
  -- now deal with all cases using tactics
  all_goals {
    -- we can try rewriting either (a ff) or (a tt) which must occur
    -- in the goal expression because of the original (a b) expression
    -- and only one of those is present, so we use the
    -- <|> syntax to try the second tactic (rw) if the first one fails
    rw ht <|> rw hf,
    -- now, either we've formed a reflexive equality and we're done
    -- or the equality we're left with is of the form (a tt = ff)
    -- which we'll have as an assumption
    -- if tactic we tried to use here was a plain "assumption",
    -- that would fail in the cases where we had already solved the goal
    -- so we wrap it in a "try"
    try { assumption } },
end

Answer 2

这是一个作弊的解决方案：

import tactic.fin_cases                                                                                                                 
                                                                                                                                        
example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=                                                                           
begin                                                                                                                                   
  intros a b,                                                                                                                           
  fin_cases a; fin_cases b; refl                                                                                                        
end

这fin_cases是来自 的一个策略mathlib。它对a : α是否可以找到可计算的[fintype α]. 因此，从数学上讲，解决方案是：考虑所有情况，验证在每种情况下我们都有一个定义相等。

Answer 3

这对我来说是一个非常不寻常的问题（我是一名数学家，所以bool对我来说不存在），所以我可能错过了解决问题的有效方法，但你当然可以对a tt,a ff和b.

example : ∀ a : bool → bool, ∀ b : bool, a (a (a b)) = a b :=
begin
     assume a b,
     cases h₁ : a tt ; 
     cases h₂ : a ff ;  
     cases b,
     repeat { rw h₁ <|> rw h₂ },
end

（在编辑中略微简化）

不要犹豫，询问部分语法是否不清楚（或者更好，来询问Zulip）。

我不确定你在尝试中做了什么。但是您的行在您的上下文中cases a:b创建了一个新事物a，这很可能会引起混淆。而战术成功的事实contradiction是不幸的意外，在trivial这里使用会更清楚。