Как работает дискриминационная тактика?

Давайте пройдемся по этому l1 термину и опишем каждую его часть.

l1 : A = B -> False

l1 - это импликация, следовательно, согласно соответствию Карри-Ховарда, это абстракция (функция):

fun H : A = B =>

Теперь нам нужно построить тело нашей абстракции, которое должно иметь тип False. Тактика discriminate предполагает реализацию тела как приложения f x, где f = fun H0 : False => False_ind False H0 и это просто оболочка вокруг принципа индукции для False, который гласит, что если у вас есть доказательство False, вы можете получить доказательство любого предложения, которое захотите (False_ind : forall P : Prop, False -> P ):

(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)

Если мы выполним один шаг бета-редукции, мы упростим приведенное выше до

False_ind False
          (eq_ind A
             (fun e : AB => match e with
                            | A => True
                            | B => False
                           end) I B H)

Первый аргумент False_ind - это тип создаваемого нами термина. Если бы вы доказали A = B -> True, это было бы False_ind True (eq_ind A ...).

Между прочим, легко увидеть, что мы можем еще больше упростить наше тело - чтобы False_ind работало, ему нужно предоставить доказательство False, но это именно то, что мы пытаемся построить здесь! Таким образом, мы можем полностью избавиться от False_ind, получив следующее:

eq_ind A
  (fun e : AB => match e with
                 | A => True
                 | B => False
                 end) I B H

eq_ind - это принцип индукции для равенства, гласящий, что равные могут быть заменены равными:

eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
   P x -> forall y : A, x = y -> P y

Другими словами, если есть доказательство P x, то для всех y, равных x, P y выполняется.

Теперь давайте шаг за шагом создадим доказательство False, используя eq_ind (в итоге мы должны получить eq_ind A (fun e : AB ...) член).

Мы начинаем, конечно, с eq_ind, затем применяем его к некоторому x - давайте использовать A для этой цели. Далее нам понадобится предикат P. При записи P нужно помнить одну важную вещь: мы должны быть в состоянии доказать P x. Этой цели легко достичь - мы собираемся использовать предложение True, которое имеет тривиальное доказательство. Еще одна вещь, о которой следует помнить, - это утверждение, которое мы пытаемся доказать (False) - мы должны возвращать его, если входной параметр не равен A. При всем вышесказанном предикат почти сам записывается:

fun x : AB => match x with
              | A => True
              | B => False
              end

У нас есть первые два аргумента для eq_ind и нам нужны еще три: доказательство для ветви, где x равно A, что является доказательством True, то есть I. Некоторые y, которые приведут нас к утверждению, которое мы хотим получить доказательство, то есть B, и доказательству того A = B, которое называется H в самом начале этого ответа. Складывая их друг на друга, мы получаем

eq_ind A
       (fun x : AB => match x with
                  | A => True
                  | B => False
                  end)
       I
       B
       H

И это именно то, что нам дал discriminate (по модулю некоторой упаковки).

Другой ответ касается разборчивой части, я сосредоточусь на ручном доказательстве. Ты пытался:

Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined.

Что следует отметить и заставляет меня часто чувствовать себя некомфортно при использовании Coq, так это то, что Coq принимает неточно определенные определения, которые он внутренне переписывает в хорошо типизированные термины. Это позволяет быть менее подробным, поскольку Coq добавляет некоторые части. Но с другой стороны, Coq манипулирует термином, отличным от того, который мы ввели.

Это ваше доказательство. Естественно, сопоставление с образцом на e должно включать конструктор eq_refl, который является единственным конструктором типа eq. Здесь Coq обнаруживает, что равенство не используется, и, таким образом, понимает, как изменить ваш код, но то, что вы ввели, не является правильным сопоставлением с образцом.

Два ингредиента могут помочь понять, что здесь происходит:

• определение eq
• полный синтаксис сопоставления с образцом с условиями as, in и return

Во-первых, мы можем взглянуть на определение eq.

Inductive eq {A : Type} (x : A) : A -> Prop :=  eq_refl : x = x.

Обратите внимание, что это определение отличается от того, которое кажется более естественным (во всяком случае, более симметричным).

Inductive eq {A : Type} : A -> A -> Prop :=  eq_refl : forall (x:A), x = x.

Это действительно важно, чтобы eq определялся первым определением, а не вторым. В частности, для нашей проблемы важно то, что в x = y x является параметром, а y - индексом. То есть x является постоянным для всех конструкторов, а y может отличаться в каждом конструкторе. У вас такая же разница с типом Vector.t. Тип элементов вектора не изменится, если вы добавите элемент, поэтому он реализован как параметр. Однако его размер может меняться, поэтому он реализован в виде индекса.

Теперь давайте посмотрим на расширенный синтаксис сопоставления с образцом. Я даю здесь очень краткое объяснение того, что я понял. Не стесняйтесь обращаться к справочному руководству для получения более безопасной информации. . Предложение return может помочь указать тип возвращаемого значения, который будет отличаться для каждой ветви. В этом предложении могут использоваться переменные, определенные в предложениях as и in сопоставления с образцом, которое связывает, соответственно, согласованный термин и индексы типа. Предложение return будет интерпретироваться в контексте каждой ветви, заменяя переменные as и in, используя этот контекст, для проверки типов ветвей одну за другой и использовать для ввода match с внешней точки зрения.

Вот надуманный пример с предложением as:

Definition test n :=
  match n as n0 return (match n0 with | 0 => nat | S _ => bool end) with
  | 0 => 17
  | _ => true
  end.

В зависимости от значения n мы не возвращаем один и тот же тип. Тип test - forall n : nat, match n with | 0 => nat | S _ => bool end. Но когда Coq может решить, в каком случае совпадение мы, он может упростить тип. Например:

Definition test2 n : bool := test (S n).

Здесь Coq знает, что, что бы ни было n, S n, заданное test, будет иметь результат типа bool.

Для равенства мы можем сделать нечто подобное, на этот раз используя предложение in.

Definition test3 (e:A=B) : False :=
  match e in (_ = c) return (match c with | B => False | _ => True end) with
  | eq_refl => I
  end.

Что тут происходит ? По сути, Coq проверяет типы отдельно ветвей match и самого match. В единственной ветви eq_refl, c равно A (из-за определения eq_refl, который создает экземпляр индекса с тем же значением, что и параметр), поэтому мы заявили, что вернули некоторое значение типа True, здесь I. Но если смотреть со стороны, c равно B (потому что e относится к типу A=B), и на этот раз предложение return утверждает, что match возвращает некоторое значение типа False. Здесь мы используем возможности Coq для упрощения сопоставления с образцом в типах, которые мы только что видели с test2. Обратите внимание, что мы использовали True в других случаях, кроме B, но нам не нужен True в частности. Нам нужен только какой-то жилой тип, чтобы мы могли вернуть что-то в ветке eq_refl.

Возвращаясь к странному термину, созданному Coq, метод, используемый Coq, делает нечто подобное, но в этом примере, безусловно, более сложное. В частности, Coq часто использует типы IDProp, населенные idProp, когда ему нужны бесполезные типы и термины. Они соответствуют True и I, использованным выше.

Наконец, я даю ссылку на обсуждение coq-club, которое действительно помогло мне понять, как расширенное сопоставление шаблонов набирается в Coq.