gds (gds) wrote,
gds
gds

coq, true_neq_false

Кое в чём разобрался, близко к прошлой проблеме.
А вы посмотрите, правильно ли.

Definition true_neq_false
 : true <> false


 :=
  fun H : true = false =>
  eq_ind
    true
    (fun b : bool =>
       if b then True else False)
    I
    false
    H
.


Итак, что здесь творится, насколько я понимаю.
Есть гипотеза, являющаяся неравенством (хотя, как понимаю, достаточно будет того, что coq развернёт "true <> false" -> "not (true = false)" -> "(true = false) -> False"; но не уверен, что всё обстоит именно так, как я говорю).
Далее, это логическое утверждение действительно переписывается в "(true = false) -> False" (проверил тактикой "refine (fun H => _)"), и в гипотезе H у нас действительно "true = false".
И с этим равенством надо работать. Идея -- поработать индуктивно.
Check eq_ind.
eq_ind
     : forall (A : Type (* Coq.Init.Logic.12 *)) (x : A) (P : A -> Prop),
       P x -> forall y : A, @eq A x y -> P y

Это -- описание индукции, которую можно провести, имея какое-либо равенство. По-человечески здесь написано такое: "для любого типа A, если для x:A верно заданное свойство P x, то для всех y:A, которые равны x (т.е. для которых есть утверждение "eq x y") будет верно свойство P y".

"A" является implicit argument, и формы записи "@eq_ind bool true ..." и "eq_ind true ..." равны настолько, насколько coq сможет вывести этот самый bool. А тут проблем нет, так как по типу x этот bool выводится хорошо.

Ранее мне было неочевидно, что, пытаясь вывести False:Prop, нужно делать индукцию по свойствам, которые возвращают Prop. Теперь уже понял. То есть, в качестве свойства P в индукцию передаём (fun b : bool => if b then True else False).

Далее, утверждаем, что свойство P x (тут -- "P true" = "True") действительно при вычислении имеет тип True, и значение типа True, единственное, которое "I", передаём в индукцию.

Далее передаём аргумент y, равный false, и за ним -- утверждение "@eq bool x y" = "eq x y" = "x = y" = "true = false" = H -- то, которое приняли как аргумент доказательства.

И вот, coq в качестве результата индукции по равенству вычисляет и выдаёт нам результат "P y", а именно, факт того, что в данных логических допущениях верно утверждение "P y" = "P false" = "if false then True else False" = "False". Это утверждение и является результатом применения индукции, и всё выражение вычисляется в False.

То есть, имея на входе утверждение "true = false", имеем на выходе False.

Как же долго я всё это пытался понять.

CPDT помогает, если её читать, а не листать.
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments