Хранение информации при использовании индукции? - PullRequest
Новая
       6

Хранение информации при использовании индукции?

14 голосов
/ 23 декабря 2010

Я использую Coq Proof Assistant для реализации модели (небольшого) языка программирования (расширение реализации Featherweight Java Бруно Де Фрейна, Эрика Эрнста, Марио Зюдхолта).Одна вещь, которая продолжает появляться при использовании тактики induction, - как сохранить информацию, заключенную в конструкторы типов.

У меня есть подпечатка Prop, реализованная как 

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

, где extends - это механизм расширения класса, видимый в Java, а typ представляет два различных типа доступных типов, 

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

Примером, где я хотел бы сохранить информацию о типе, является использование induction тактика на основе гипотезы типа 

H: sub_type (c_typ u) (c_typ v)

Например, 

u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

с использованием induction H. отбрасывает всю информацию о u и v.Случай st_refl становится 

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

. Как видите, информация о том, что u и v связаны с конструкторами typ в H и, следовательно, с t, равнапотерял.Хуже всего то, что из-за этого Coq не может видеть, что u и v должны фактически быть одинаковыми в этом случае.

При использовании тактики inversion на H Coq успешновидя, что u и v одинаковы.Однако эта тактика здесь неприменима, поскольку мне нужны гипотезы индукции, которые генерирует induction, чтобы доказать случаи st_trans и st_extends.

Существует ли тактика, сочетающая в себе лучшее из inversion иinduction чтобы генерировать гипотезы индукции и получать равенства, не уничтожая информацию о том, что заключено в конструкторы?В качестве альтернативы, есть ли способ вручную получить нужную мне информацию?info inversion H и info induction H показывают, что многие преобразования применяются автоматически (особенно с inversion).Это привело меня к эксперименту с тактикой change вместе со строительством let ... in, но без какого-либо прогресса.

Ответы [ 3 ]

14 голосов
/ 24 декабря 2010

Это общая проблема, когда вам нужно ввести гипотезу с зависимым типом (sub_type (c_typ u) (c_typ v)), параметры которого имеют определенную структуру (c_typ u).Существует общая хитрость, которая заключается в том, чтобы выборочно переписать структурный параметр в переменную, сохраняя равенство в среде. 

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1.
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2.
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).

Начиная с Coq 8.2, этот общий шаблон set-assert-clearbody выполняетсявстроенная тактика remember <em>term</em> as <em>ident</em> in *goal_occurences*.

Вот глупая лемма, доказанная с помощью этой тактики. 

Lemma subtype_r_left_equal :
  forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2.
Proof.
  intros.
  remember (r_typ r1) as t1 in H.
  induction H.
  congruence.
  solve [firstorder].
  discriminate.
Qed.

Бонусный совет (из опыта, но это было давно, поэтому я неt запомните детали): когда вы делаете довольно синтаксические рассуждения о системах типов (что обычно бывает при выполнении подобных видов механических доказательств), может быть удобно продолжать вводить суждения в Set.Подумайте о наборе деривации как об объектах, о которых вы рассуждаете.Я помню случаи, когда было удобно вводить равенства при типизации деривации, что не всегда работает с типизацией дериваций в Prop.

С вашим Problem.v, вот доказательство случая рефлексивности,Для транзитивности, я подозреваю, что ваша индукционная гипотеза недостаточно сильна.Это может быть побочным продуктом того, как вы упростили проблему, хотя транзитивность часто требует неожиданно включенных гипотез индукции или лемм. 

Fact sub_type_fields: forall u v fsv,
  sub_type (c_typ u) (c_typ v) -> fields v fsv ->
  exists fs, fields u (fsv ++ fs).
Proof.
  intros.
  remember (c_typ u) as t1 in H.
  remember (c_typ v) as t2 in H.
  induction H.
  (* case st_refl *)
  assert (v = u). congruence. subst v t.
  exists nil. rewrite <- app_nil_end. assumption.
  (* case st_trans *)
  subst t1 t3.
  (* case st_extends *)
Admitted.
5 голосов
/ 04 февраля 2011

Я столкнулся с подобной проблемой, и тактика "зависимой индукции" Coq 8.3 позаботилась о бизнесе.

3 голосов
/ 01 мая 2016

Я был уверен, что у CPDT были некоторые комментарии по этому вопросу, но не совсем очевидно, где это.Вот некоторые ссылки:

  1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html Раздел «Предикаты с неявным равенством» показывает, пожалуй, самый простой случай, когда Coq «теряет информацию» (при разрушении, а не прииндукция.) Это также объясняет, ПОЧЕМУ эта информация потеряна: когда вы уничтожаете тип, примененный к аргументу, который не является свободной переменной, эти типы сначала заменяются свободными переменными (именно поэтому Coq теряет информацию.)

  2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html В разделе «Методы ухода от аксиом» показаны некоторые приемы обхода аксиомы K, в том числе «трюк равенства», описанный Жилем.Ищите «использование общего трюка, основанного на равенстве, для поддержки наведения на не переменные аргументы для семейств типов»

Я думаю, что это явление тесно связано с сопоставлением зависимых паттернов.

...