Принцип индукции, генерируемый Coq, ведет себя не так, как я хочу

Question

Отредактировано для понятности

Я пытаюсь доказать свойства дерева особого типа. Это дерево похоже на следующее. Проблема в том, что принцип индукции, сгенерированный Coq, недостаточен для доказательства свойств дерева. Для более простого примера, скажем, следующий тип описывает все мои "деревья":

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

Затем, чтобы доказать правильность всех деревьев (скажем, для импликации), мне нужно доказать следующую лемму:

Lemma soundness: forall E:BES, forall f g:Prop, forall R G:propVar_relation, 
  (prv_tree E (G |- f ---> g)) -> (E,G,R |= f --> g).

Для чего мне нужно применить индукцию на структуру дерева. Однако, если я сделаю intros;induction H. тогда первая подзадача (E,G,R |= f --> g) т.е. информация о требуемой структуре f и g теряется (хотелось бы (E,G,R |= a --> a)). (Также для индуктивного случая гипотеза индукции утверждает, (E,G,R |= f --> g)что странно для меня).

Еще один подход, который я попробовал, это вспомнить (G |- f ---> g), чтобы сохранить структуру f и g доступной. Доказательство тогда продолжается как intros;remember (G |- f --> g) as stmt in H.induction H. Затем я получаю цели и условия, которые я ожидаю для своих базовых случаев. Однако для доказательства случая TRA я получаю следующий контекст доказательства:

H : prv_tree E (G0 |- a --> b)
H0 : prv_tree E (G0 |- b --> c)
IHprv_tree1 : G0 |- a --> b = G |- f --> g -> (E,G,R |= f --> g)
IHprv_tree2 : G0 |- b --> c = G |- f --> g -> (E,G,R |= f --> g)

В то время как я ожидаю, что гипотеза индукции будет

IHprv_tree1 : prv_tree E (G0 |- a --> b) -> (E,G,R |= a --> b)
IHprv_tree2 : prv_tree E (G0 |- b --> c) -> (E,G,R |= b --> c)

СТАРЫЙ ТЕКСТ

Я пытаюсь доказать свойства дерева особого типа. Это дерево может быть построено с использованием 21 различных правил (которые я не буду повторять здесь). Проблема в том, что принцип индукции, сгенерированный Coq, недостаточен для доказательства свойств дерева.

Дерево строится следующим образом

Inductive prv_tree (E:BES): (*BES ->*) statement -> Prop := 
.... (*constructors go here*).

Один из этих конструкторов

CTX: forall a b c:propForm, forall x:propVar, forall G:propVar_relation,
  (prv_tree E (makeStatement G a b) -> 
    (prv_tree E (makeStatement G (replace c x a) (replace c x b))))

Моя цель - доказать

Lemma soundness: forall E:BES, forall f g:propForm, forall G:propVar_relation, 
  forall tree:prv_tree E (makeStatement G f g), rel_cc_on_propForm E (cc_max E) G f g.

Для этого я помню makeStatement G f g в противном случае я теряю информацию о структуре f и g. Затем я применяю индукцию к дереву. Я доказал все случаи как отдельные леммы, которые я могу успешно использовать для базовых случаев. Однако для индуктивных случаев гипотеза об индукции, представленная мне Коком, непригодна.

Например, для упомянутого выше конструктора CTX я получаю следующую индукционную гипотезу:

IHP {| context := G; stm_l := a; stm_r := b |} =
  {| context := empty_relation; stm_l := replace c x a;
  stm_r := replace c x b |} ->
    E, cc_max E |- replace c x a <,_ empty_relation replace c x b

который я не могу использовать. Вместо этого я хочу что-то вроде

IHP prv_tree E {| context := G; stm_l := a; stm_r := b |} ->
  E, cc_max E |- replace c x a <,_ empty_relation replace c x b

Может кто-нибудь объяснить мне, как это исправить? До сих пор я пытался определить свой собственный принцип индукции на prv_tree, однако это приводит к тем же проблемам, так что, возможно, я сделал это неправильно?

Утверждение для CTX в моем собственном принципе индукции следующее:

  (forall a b c:propForm, forall x:propVar, forall G:propVar_relation, 
    (prv_tree E {| context := G; stm_l := a; stm_r := b |} ) ->
      P {| context := G; stm_l := replace c x a; stm_r := replace c x b |})

Answer 1

Я думаю, что я понял вашу проблему, но мне пришлось заполнить весь ваш вопрос. Было бы проще, если бы вы придумали самостоятельный пример, как предложил @ejgallego.

Вот как я смоделировал вашу проблему:

Axiom BES : Type.
Axiom propVar_relation : Type.

Inductive statement :=
| Stmt : propVar_relation -> Prop -> Prop -> statement.

Notation "G |- a ---> b" := (Stmt G a b) (at level 50).

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

Lemma soundness: forall (E: BES) (f g:Prop) (R G:propVar_relation),
  (prv_tree E (G |- f ---> g)) -> R = R.

Действительно, мы сталкиваемся с теми же проблемами, что и те, которые вы описали в своем вопросе. Решение состоит в том, чтобы revert после запоминания и перед выполнением индукции.

intros.
remember (G |- f ---> g) as stmt. revert f g R G Heqstmt.
induction H; intros.

Теперь гипотезы индукции все еще странные, но они должны работать.

Answer 2

Спасибо за помощь. В конце концов я нашел решение сам. Хитрость заключалась в определении вспомогательной функции h:statement -> Prop, как и следовало ожидать по принципу индукции, и использовать эту функцию вместо (E,G,R |= f --> g),