Есть ли какая-то тактика для доказательства этой по-видимому легкой цели? - PullRequest
Новая
       12

Есть ли какая-то тактика для доказательства этой по-видимому легкой цели?

0 голосов
/ 12 апреля 2019

У меня есть следующая цель:

1 подцель

______________________________________ (1/1)

(если (a =? A)% string || false тогда # a :: nil else nil) = nil

Поскольку, очевидно, a = a, мне интересно, почему тактика "упрощения" не работает.

1 Ответ

2 голосов
/ 12 апреля 2019 
Print "=?".

String.eqb = 
fix eqb (s1 s2 : string) {struct s1} : bool :=
  match s1 with
  | "" => match s2 with
          | "" => true
          | String _ _ => false
          end
  | String c1 s1' =>
      match s2 with
      | "" => false
      | String c2 s2' => if Ascii.eqb c1 c2 then eqb s1' s2' else false
      end
  end
     : string -> string -> bool

String.eqb определяется как fix, что означает, что Coq не будет сводить его применение к аргументу, если Coq не может увидеть символ головы (конструктор) этого аргумента. В этом случае тактика simpl не может применяться String.eqb a a, поскольку a является переменной, мы ничего не знаем о ее «форме» - следовательно, вы ничего не видите.

Кстати, функция ||, т.е. orb определяется сопоставлением с образцом по первому аргументу, поэтому simpl не может уменьшить (a =? a)%string || false до (a =? a)%string.

Выход здесь - переписать лемму String.eqb_refl, после использования этой леммы будет совершенно очевидно, что цель недоказуема, если у вас нет противоречий в контексте, и в этом случае вам действительно не нужно String.eqb_refl.

...