A simple Coq practice session

practice_coq_1.v

(* Context와 state가 있는 프로그래밍 언어를 정형화하고자 합니다.
   프로그래밍 변수로는 De Brujin index를 사용할 것이며, 
   따라서 context는 단순히 데이터 타입들의 리스트 입니다.
   (예를 들어서 int :: int :: boolean :: nil 이 하나의 context입니다.
   리스트를 사용해서 생기는 문제를 해결해 봅시다. 
    
   16 April 2023 -- Sewon Park *)

Require Import List.

(* datatype 이라는 타입이 있다고 가정합니다. *)
Parameter datatype : Type.

(* ctx는 데이타 타입의 리스트로 정의합니다. *)
Definition ctx := list datatype.

(* 각 데이터 타입에 대해서 Coq의 타입을 하나 매칭해 주는 것이 
   데이터 타입의 denotational semantics 입니다.
   임의의 denotational semantics가 있다고 가정합니다. *)
Parameter sem_datatype : datatype -> Type.

(* 가정한 데이터 타입의 denotational semantics에 대해서
   context의 denotational semantics를 가장 단순하게,
   cartesian product로 정의합니다. 
   예를 들어서 Γ ::= int :: int :: boolean :: nil 라는 context의 
   denotation은 Z * Z * bool * unit 이 될 것입니다. 
   Denotation 타입의 term이 각 state가 됩니다.
   예를 들면, (42, 7, true, tt)는 하나의 state입니다. *)
Fixpoint sem_ctx (Γ : ctx) : Type :=
  match Γ with
  | nil => unit
  | τ :: Γ' => sem_datatype τ * sem_ctx Γ'
  end.


(* 프로그래밍 언어를 정형화하다보면 context를 합쳐야하는 경우가 있습니다.
   (Context Γ에 대해서 γ ∈ Γ를 γ : sem_ctx Γ로 써봅시다.)
   예를 들면, 계산 c1과 c2를 동시에 하고, c1의 결과 γ ∈ Γ와 c2의 결과 δ ∈ Δ를 합치는 경우입니다.
   우리는 list를 사용하니, context는 단순히 Γ ++ Δ로 합칠 수 있겠네요!
   state도 합쳐봅시다. *)
Definition sem_ctx_prod_to_app Γ Δ : (sem_ctx Γ) * sem_ctx Δ -> sem_ctx (Γ ++ Δ).
Proof.
  intros γδ.
  induction Γ.
  {    
    (* base case *)
    simpl; destruct γδ as [_ δ].
    exact δ.
  }
  {
    (* step case *)
    simpl; destruct γδ as [[x γ] δ].
    split.
    exact x.
    exact (IHΓ (γ, δ)).
  }
Defined.

Notation " ( γ ; δ ) " := (sem_ctx_prod_to_app _ _  (γ, δ)).

(* 이제 계산 결과 γ ∈ Γ와 δ ∈ Δ가 있을 경우, (γ; δ) ∈ Γ ++ Δ 로 합칠 수 있습니다.
   
   사실 정말 문제는 3개 (이상)의 결과를 합칠 경우 입니다.
   γ1 ∈ Γ1, γ2 ∈ Γ2, γ3 ∈ Γ3 가 있을 때, 합치는 방법으로 2개가 있습니다.
   
   - ((γ1 ; γ2) ; γ3) ∈ (Γ1 ++ Γ2) ++ Γ3 
   - (γ2 ; (γ2 ; γ3)) ∈ Γ1 ++ (Γ2 ++ Γ3)
   
   안타깝게도 두 결과가 같다는 것을 보일 수 없습니다. 타입이 다르니까요:

   ((γ1 ; γ2) ; γ3) : sem_ctx ((Γ1 ++ Γ2) ++ Γ3)
   (γ2 ; (γ2 ; γ3)) : sem_ctx (Γ1 ++ (Γ2 ++ Γ3))

   
   하지만, 그럼에도 두 결과들이 어떤 식으로든 뭔가 같다는 것을 보여야 합니다.
   나중에 semantics를 정의하고 soundness를 증명할 때 분명히 필요할 것 입니다.
   
   Q. 관련하여 어떤 정리를 증명할 수 있을까요?



   [...]


















   생각에 도움이 되는 음악
   https://www.youtube.com/watch?v=T--6HBX2K4g




   

























  사실 DTT를 사용하다보면 흔히 있는 경우 입니다.
  a : A 와 b : B가 있고, eq : A = B가 있을 때 a = b 임을 말하고 싶습니다. 
  하지만, 엄밀히 말하자면, A = B 는 propositional equality이며
  syntactic하게 A와 B는 다른 타입입니다. 따라서, a = b는 옳지 못한 표현이 됩니다.

  잘 생각해보면, "a : A"에서의 타입 A는 type universe에서의 변수 A에 dependent한 타입입니다.
  à la Tarski type universe U 를 Coq이 사용했었다면 더 명확히 볼 수 있었을 겁니다. 
  다음과 같이 써있다었면요:
         a : El A, b : El B, eq : Id U A B
  즉, El A의 term과 El B의 term을 A = B일 때 어떻게 비교할 수 있는지의 문제입니다.
  
  transport는 type family F : A -> Type 가 있을 때 A에서의 equality를 fiber 사이의 
  함수로 올려주는 연산입니다.
*)
Definition tr {A} (F : A -> Type) {x y : A} (eq : x = y) : F x -> F y.
Proof.
  intro t.
  destruct eq.
  exact t.
Defined.


(* transport 를 사용해서 a : A, b : B, eq : A = B일 때 a ≃ b 를 
   transport 된 a가 b와 같다는 것으로 정의할 수 있습니다.
   이게 아무래도 최선이겠죠?..*)
Definition eq_tr {A B : Type} (a : A) (b : B) (eq : A = B) : Type
  := tr (fun T : Type => T) eq a = b.


(* 다시 원래 문제로 돌아와서, Γ1 Γ2 Γ3가 있을 때 Γ1 ++ (Γ2 ++ Γ3) = (Γ1 ++ Γ2) ++ Γ3 
   는 이미 List 에 증명되어 있습니다. 
   app_assoc 입니다만, Qed. 로 증명되어서 정의를 사용할 수 없으니, 그대로 다시 정의해봅시다. *)
Definition app_assoc := 
fun {A : Type} (l m n : list A) =>
list_ind (fun l0 : list A => l0 ++ m ++ n = (l0 ++ m) ++ n)
  ((let H : n = n := eq_refl in
    (let H0 : m = m := eq_refl in
     (let H1 : A = A := eq_refl in (fun (_ : A = A) (_ : m = m) (_ : n = n) => eq_refl) H1) H0) H)
   :
   nil ++ m ++ n = (nil ++ m) ++ n)
  (fun (a : A) (l0 : list A) (IHl : l0 ++ m ++ n = (l0 ++ m) ++ n) =>
   (let H : l0 ++ m ++ n = (l0 ++ m) ++ n := IHl in
    (let H0 : a = a := eq_refl in
     (let H1 : A = A := eq_refl in
      (fun (_ : A = A) (_ : a = a) (H4 : l0 ++ m ++ n = (l0 ++ m) ++ n) =>
       eq_trans (f_equal (fun f : list A -> list A => f (l0 ++ m ++ n)) eq_refl) (f_equal (cons a) H4)) H1) H0) H)
   :
   (a :: l0) ++ m ++ n = ((a :: l0) ++ m) ++ n) l.


(* app_assoc Γ1 Γ2 Γ3 : Γ1 ++ (Γ2 ++ Γ3) = (Γ1 ++ Γ2) ++ Γ3 의 ctx에서의 equality를 
   sem_ctx : ctx -> Type에 대해서 lift 하면
   
   f_equal sem_ctx (app_assoc Γ1 Γ2 Γ3) : sem_ctx (Γ1 ++ (Γ2 ++ Γ3)) = sem_ctx ((Γ1 ++ Γ2) ++ Γ3)

   가 되고, 

   (γ1; (γ2; γ3)) : sem_ctx (Γ1 ++ (Γ2 ++ Γ3))
   ((γ1; γ2); γ3) : sem_ctx ((Γ1 ++ Γ2) ++ Γ3)

   이니, 앞서 정의한 eq_tr을 사용해서 (γ1; (γ2; γ3)) 와 ((γ1; γ2); γ3)가 "뭔가 같다"를 정의할 수 있겠네요!
   

   Q. 즉, 우리가 증명하고 싶은, "c1 c2를 합치고 c3를 합치나 c2 c3을 합친 것에 c1을 합친거나 같다"는 
   정리는 다음과 같습니다. 증명해봅시다!  *)
Fixpoint app_assoc_eq_tr (Γ1 Γ2 Γ3 : ctx) : forall (γ1 : sem_ctx Γ1) (γ2 : sem_ctx Γ2) (γ3 : sem_ctx Γ3),
    eq_tr (γ1 ; (γ2 ; γ3)) ((γ1 ; γ2) ; γ3) (f_equal sem_ctx (app_assoc Γ1 Γ2 Γ3)).



  
  (* 보조 정리들을 몇 가지를 먼저 증명해야 할 수 있습니다. 
     
     아래에 제가 어떤 보조 정리들을 먼저 증명했는지 힌트로 적어놨습니다. (증명 제외).

     제 풀이는 그 아래에 있습니다! *)




















  



(* 생각에 도움이 되는 음악
   https://www.youtube.com/watch?v=R1vmfVpINbk *)






  





























Admitted.









(* 본 증명에 앞서서 저는 다음의 정리들을 먼저 증명해서 사용했습니다
   이 아래에는 제 증명이 있습니다. *)

Lemma tr_constant_pair : forall X (P : X -> Type) C (x y : X) (p : x = y),
  forall c t, tr (fun x => C * P x)%type p (c, t) = (c, tr P p t).
Proof.
Admitted.

Lemma tr_f_equal : forall X Y (P : Y -> Type) (f : X -> Y) (x y : X) (p : x = y),
  forall t, tr P (f_equal f p) t = tr (fun x => P (f x)) p t.
Proof.
Admitted.

Lemma eq_refl_left_unit : forall X (x z : X) (p : x = z), eq_trans (eq_refl x) p = p.
Proof.
Admitted.
































(* 생각에 도움이 되는 음악
   https://www.youtube.com/watch?v=SX_ViT4Ra7k *)































(* 제가 증명한 방식은요~ *)
Lemma tr_constant_pair' : forall X (P : X -> Type) C (x y : X) (p : x = y),
  forall c t, tr (fun x => C * P x)%type p (c, t) = (c, tr P p t).
Proof.
  intros.
  destruct p.
  simpl.
  reflexivity.
Defined.

Lemma tr_f_equal' : forall X Y (P : Y -> Type) (f : X -> Y) (x y : X) (p : x = y),
  forall t, tr P (f_equal f p) t = tr (fun x => P (f x)) p t.
Proof.
  intros.
  destruct p.
  simpl.
  reflexivity.
Defined.

Lemma eq_refl_left_unit' : forall X (x z : X) (p : x = z), eq_trans (eq_refl x) p = p.
Proof.
  intros.
  destruct p.
  simpl.
  reflexivity.
Defined.

Fixpoint app_assoc_eq_tr' (Γ1 Γ2 Γ3 : ctx) : forall (γ1 : sem_ctx Γ1) (γ2 : sem_ctx Γ2) (γ3 : sem_ctx Γ3),
    eq_tr (γ1 ; (γ2 ; γ3)) ((γ1 ; γ2) ; γ3) (f_equal sem_ctx (app_assoc Γ1 Γ2 Γ3)).
Proof.
  intros.
  destruct Γ1.
  {
    (* when Γ1 is nil *)
    simpl; reflexivity.
  }

  {
    (* when Γ1 is cons *)
    destruct γ1 as [x γ1].
    unfold eq_tr; simpl.
    pose proof (tr_f_equal' _ _ (fun T => T) sem_ctx _ _ (eq_trans eq_refl (f_equal (cons d) (app_assoc Γ1 Γ2 Γ3)))) as rew; simpl in rew; rewrite rew; clear rew.
    
    rewrite eq_refl_left_unit'.
    rewrite tr_f_equal'.
    simpl.
    rewrite tr_constant_pair'.
    apply f_equal.
    rewrite <- app_assoc_eq_tr.
    rewrite  tr_f_equal'.
    reflexivity.
  }
Defined.