Цикл при доказательстве теоремы

Я пытаюсь доказать следующую теорему после формализации лямбда-исчисления с индексами Дебройна и заменой в Coq.

Theorem atom_equality : forall e : expression , forall x : nat,
  (beta_reduction (Var x) e) -> (e = Var x).

и это определения выражения и бета-редукции


Inductive expression : Type :=
  | Var (n : nat)
  | Abstraction (e : expression)
  | Application (e1 : expression) (e2 : expression).
.
.

Inductive beta_reduction : expression -> expression -> Prop :=
  | beta_1step (x y : expression) : beta_1reduction x y -> beta_reduction x y
  | beta_reflexivity (x : expression) :  beta_reduction x x 
  | beta_transitivity (x y z : expression) : beta_reduction x y -> beta_reduction y z -> beta_reduction x z.

Я застрял в петле, пытаясь доказать эту теорему.

Proof.
intro e. induction e.
  - intros. inversion H.

После применения этих шагов, это гипотеза и подцели, с которыми я должен работать.

3 subgoals
n, x : nat
H : beta_reduction (Var x) (Var n)
x0, y : expression
H0 : beta_1reduction (Var x) (Var n)
H1 : x0 = Var x
H2 : y = Var n
______________________________________(1/3)
Var n = Var x
______________________________________(2/3)
Var n = Var n
______________________________________(3/3)
Var n = Var x

Я могу решить первую подцель с помощью тактики инверсии H0, а вторую подцель с помощью рефлексивности. Однако, когда я достигаю третьей подцели, это то, что у меня остается.

1 subgoal
n, x : nat
H : beta_reduction (Var x) (Var n)
x0, y, z : expression
H0 : beta_reduction (Var x) y
H1 : beta_reduction y (Var n)
H2 : x0 = Var x
H3 : z = Var n
______________________________________(1/1)
Var n = Var x

Это именно то, с чего я начал. Мне нужно будет доказать, что y может принимать только значение Var x для H0, чтобы быть доказуемым.

(beta_1reduction — это одноступенчатая бета-редукция лямбда-исчисления, а beta_reduction — его рефлексивное, транзитивное закрытие)


theorem-proving coq lambda-calculus proof
person Shubham Sondhi    schedule 02.04.2021    source источник
comment
Не могли бы вы также добавить определение beta_1reduction, чтобы сделать ваш код stackoverflow.com/help/minimal-reproducible-example   -  person larsr    schedule 02.04.2021

Ответы (2)


arrow_upward
1
arrow_downward

Вы застряли, потому что инверсии на H недостаточно. Вместо этого вам понадобится своего рода индукция по H, чтобы предоставить вам необходимую гипотезу в транзитивном случае, чтобы вы могли сделать вывод. Однако, поскольку тип H является индуктивным предикатом, индукция по нему сложна. Действительно, если вы используете обычный induction H., Coq потеряет всю информацию об индексах в типе H, и особенно Var x. Это сделает ваши попытки доказательства неудачными.

Вместо этого вы можете использовать тактику dependent induction (вам потребуется Require Import Program.Equality, чтобы иметь доступ к этой тактике). Эта тактика автоматически обрабатывает тип индукции по индуктивным предикатам, где индексы не являются переменными. Здесь вы можете начать доказательство с intros e n H. dependent induction H., а остальное должно быть легко.

В общем, когда вы определяете индуктивные предикаты (такие как beta_reduction) над индуктивными типами данных (такими как expression) и хотите использовать гипотезу, используя эти индуктивные предикаты (здесь H), выполняя индукцию непосредственно по предикату (используя dependent induction), как мы это делали здесь очень мощно. В частности, он специализируется на том, какие конструкторы вашего типа данных могут появляться в индуктивной гипотезе, таким образом, одновременно выполняя своего рода индукцию по типу данных.

person Meven Lennon-Bertrand    schedule 02.04.2021

arrow_upward
1
arrow_downward

Ответ @ Meven - хорошее объяснение того, что не так, и дает хорошее решение. Если вы хотите сделать это без dependent induction тактики, вы можете remember потерять информацию самостоятельно.

Proof.
  (beta_reduction (Var x) e) -> (e = Var x).
  intros e x H.
  remember (Var x) as q eqn:Hq.
  induction H; rewrite Hq in *. 
  - inversion H.
  - reflexivity.
  - rewrite IHbeta_reduction1 in IHbeta_reduction2.
    apply IHbeta_reduction2.
    reflexivity.
    reflexivity.
Qed.
person larsr    schedule 02.04.2021
comment
В самом деле, и это в значительной степени магия, которую dependent induction автоматизирует за кулисами. - person Meven Lennon-Bertrand; 02.04.2021