Как построить индуктивный тип кобордизмов с помощью Coq?

Я пытаюсь построить индуктивный тип кобордизма, используя Coq, таким образом, чтобы можно было доказать некоторые свойства кобордизма (1-группоид и 2-группоид). Я использую следующий код Coq:

 Unset Automatic Introduction.
 Inductive  Topo : Set := t | nt.
 Definition F (i j : Topo) :=  
 match i, j with
 | t, t => t
 | t, nt => nt
 | nt, t => nt
 | nt, nt => nt
 end.

Я рассматриваю два вида топологий кобордизмов: тривиальную (t) и нетривиальную (nt). Тривиальные кобордизмы - это цилиндр, рассматриваемый как единица в 1-группоиде. Функция F дает композицию топологий.

Под индуктивным типом кобордизма подразумевается:

Inductive cobordisms {A} : A -> A -> Topo -> Type := idcobordism : forall
                           x : A, cobordisms x x t.

с тактикой:

Hint Resolve @idcobordism.

Ltac cobordism_induction :=
   intros; repeat progress (
   match goal with
  | [ p : cobordisms _ _ _  |- _ ] => induction p 
  | _ => idtac
  end
   ); auto.

Состав кобордизмов вводится согласно:

Definition concat {A} {x y z : A} {i j : Topo} : cobordisms x y i  -> cobordisms y z j   
 ->    cobordisms x z (F i j) .
Proof.
  cobordism_induction.
Defined.

Notation "p @ q" := (concat p q) (at level 60).

Обратное к заданному кобордизму определяется следующим образом:

Definition opposite {A} {x y : A} {i : Topo} : cobordisms x y i -> cobordisms y x i .
Proof.
  cobordism_induction.
Defined.

Notation "! p" := (opposite p) (at level 50).

До сих пор все в порядке. Но когда я пытаюсь доказать первое свойство 1-групид, а именно левое единство:

Lemma idcobordism_left_unit A (x y : A) (i : Topo) (p : cobordisms x y i) : 
           (idcobordism x)  @ p =  p.

Я получаю следующее сообщение об ошибке:

Error: In environment
A : Type
x : A
y : A
i : Topo
p : cobordisms x y i
The term "p" has type "cobordisms x y i" while it is expected to have type
"cobordisms x y (F t i)".

Тогда мой вопрос: как заставить Coq считать, что (F t i) эквивалентно i для всех i в соответствии с предыдущим определением F?


algebraic-data-types coq
person Juan Ospina    schedule 02.11.2014    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Проблема в том, что ваше определение F всегда делает match для второго аргумента, даже если это не требуется. Из-за этого F t i и i не будут по определению равны, если i не является конструктором. Решение состоит в том, чтобы изменить определение F так, чтобы желаемое равенство стало очевидным:

Definition F (i j : Topo) :=  
match i with
| t => j
| nt => nt
end.

К сожалению, вы не сможете выполнить тот же трюк, показывая правильную личность, поскольку тогда у вас возникнет обратная проблема. В этом случае решением было бы использовать явное приведение, чтобы связать оба пути:

Definition cast_cb {A} {x y : A} i : cobordisms x y (F i t) -> cobordisms x y i :=
  match i with t => fun x => x | nt => fun x => x end.

Lemma right_id A (x y : A) i (p : cobordisms x y i) :
  cast_cb i (p @ (idcobordism y)) = p.
person Arthur Azevedo De Amorim    schedule 02.11.2014

arrow_upward
1
arrow_downward

Используя стратегию, предложенную Артуром Азеведо де Амори, можно завершить доказательство 1-квазигруппоидной структуры для кобордизмов:

   (** The following lemmas say that the cobordisms form a
   1-quasi-groupoid. *)


Lemma idcobordism_left_unit A (x y : A) (i : Topo) (p : cobordisms x y i) : (idcobordism x) @ p =  p.
Proof.
  cobordism_induction.
Defined.





Definition cast_cb {A} {x y : A} i : cobordisms x y (F i t) -> cobordisms x y i :=
  match i with t => fun x => x | nt => fun x => x end.

Lemma idcobordism_right_unit A (x y : A) i (p : cobordisms x y i) :
  cast_cb i (p @ (idcobordism y)) = p.
Proof.
  cobordism_induction.
Defined.


Definition cast_cb2 {A} {x y : A} i j : cobordisms x y (F j i) -> cobordisms x y (F i j) :=
  match i,j with t,t => fun x => x | t,nt => fun x => x | nt,t => fun x => x | nt,nt => fun x => x  end.


Lemma opposite_concat A (x y z : A) (i j k : Topo) (p : cobordisms x y i) (q : cobordisms y z j) :  !(p @ q) = cast_cb2 i j (!q @ !p).
Proof.
  cobordism_induction.
Defined.




Lemma opposite_idcobordism A (x : A) : !(idcobordism x) = idcobordism x.
Proof.
  auto.
Defined.


Lemma opposite_opposite A (x y : A) (i : Topo) (p : cobordisms x y i) : !(! p) = p.
Proof.
  cobordism_induction.
Defined.

Definition cast_cb3 {A} {x y : A} i j k : cobordisms x y (F i (F j k)) -> cobordisms x y (F (F i j) k) :=
  match i,j,k with t,t,t => fun x => x | t,t,nt => fun x => x | t,nt,t => fun x => x | t,nt,nt => fun x => x 
                   | nt,t,t => fun x => x | nt,t,nt => fun x => x | nt,nt,t => fun x => x | nt,nt,nt => fun x => x end.



Lemma concat_associativity A (x y z w : A) (i j k : Topo) (p : cobordisms x y i) (q : cobordisms y z j) (r : cobordisms z w k) :
  (p @ q) @ r = cast_cb3 i j k (p @ (q @ r)).
Proof.
  cobordism_induction.
Defined.
person Juan Ospina    schedule 03.11.2014