Как расширить грамматику в coq? - PullRequest
Новая
       4

Как расширить грамматику в coq?

0 голосов
/ 09 февраля 2020 
Inductive ty0: Type :=
| Bool : ty0
| Int : ty0
| Dyn : ty0
| Arrow0: ty0 -> ty0 -> ty0.

Inductive ty1: Type := 
| ty : ty0 -> ty1
| Inters : ty1 -> ty1 -> ty1.

Inductive ty2: Type :=
| ty': ty0 -> ty2
| Arrow2 : ty1 -> ty2 -> ty2.

Inductive consist : ty2 -> ty2 -> Prop :=
 | cs_dyn1 : forall t2, consist Dyn t2

У меня есть грамматика, которая является ty0, и я хочу создать грамматику t1, которая является t0, и другие вещи. Пока у меня нет проблем с компиляцией. Но когда я определяю «состоять» и говорю consist Dyn t2, он говорит, что на самом деле Дин равен t0, и он ожидает t2. Как мне сказать, что t2 - это t0 плюс другие вещи?

Отредактированное отношение: 

Coercion ty0_ty2 (t : ty0) : ty2 := (ty' t).
Coercion ty0_ty1 (t : ty0) : ty1 := (ty t).

Inductive consist0 : ty0 -> ty0 -> Prop := 
| cs_dyn1 : forall t2, consist0 Dyn t2
| cs_dyn2 : forall t1, consist0 t1  Dyn
| cs_same : forall t1, consist0 t1 t1
| cs_arrow0 : forall t1 t2 t1' t2', consist0 t1 t1' -> 
                                    consist0 t2 t2'->
 consist0 (Arrow0 t1 t2) (Arrow0 t1' t2').

Inductive consist1 : ty1 -> ty1 -> Prop :=
| cs_same1 : forall t1, consist1 t1 t1
| cs_consist0 : forall t1 t2, consist0 t1 t2 -> consist1 t1 t2
| c_inters : forall t1 t2 t1' t2', consist1 t1 t1' -> 
consist1 t2 t2'->
consist1 (Inters t1 t2) (Inters t1' t2').

Inductive consist : ty2 -> ty2 -> Prop :=
  | cs_consist1 : forall t1 t2, consist0 t1 t2 -> consist t1 t2
  | cs_arrow2 : forall t1 t2 t1' t2', consist1 t1 t1' -> 
                                      consist t2 t2'->
   consist (Arrow2 t1 t2) (Arrow2 t1' t2').

1 Ответ

0 голосов
/ 09 февраля 2020

Вы можете определить принуждение от ty0 до ty2, и это немного поможет: 

Inductive ty0: Type :=
| Bool : ty0
| Int : ty0
| Dyn : ty0
| Arrow0: ty0 -> ty0 -> ty0.

Inductive ty1: Type :=
| ty : ty0 -> ty1
| Inters : ty1 -> ty1 -> ty1.

Inductive ty2: Type :=
| ty': ty0 -> ty2
| Arrow2 : ty1 -> ty2 -> ty2.

Coercion ty0_ty2 (t : ty0) : ty2 := (ty' t).

Inductive consist : ty2 -> ty2 -> Prop :=
 | cs_dyn1 : forall t2, consist Dyn t2.

См. https://coq.inria.fr/refman/addendum/implicit-coercions.html для получения дополнительной информации.

...