Merge pull request jwiegley#106 from jwiegley/johnw/cartesian

Author: jwiegley

Instance/Lambda/Sem.v

@@ -19,7 +19,7 @@ Fixpoint SemTy (τ : Ty) : Type :=
   | TyArrow dom cod => SemTy dom → SemTy cod
   end.
 
-Definition SemEnv Γ : Type := ilist SemTy Γ.
+Definition SemEnv Γ : Type := ilist (B:=SemTy) Γ.
 
 Fixpoint SemVar `(v : Var Γ τ) : SemEnv Γ → SemTy τ :=
   match v with

Lib/IList.v

@@ -11,15 +11,69 @@ Import ListNotations.
 Section ilist.
 
 Context {A : Type}.
-
-Variable B : A → Type.
+Context {B : A → Type}.
 
 Fixpoint ilist (l : list A) : Type :=
   match l with
   | []      => unit
   | x :: xs => B x * ilist xs
   end.
 
+Definition icons
+           (a : A)
+           {l : list A}
+           (b : B a)
+           (il : ilist l) : ilist (a :: l) :=
+  (b, il).
+
+Definition inil : ilist [] := tt.
+
+(* Get the car of an ilist. *)
+Definition ilist_hd {As : list A} (il : ilist As) :
+  match As return ilist As → Type with
+    | a :: As' => fun il => B a
+    | [] => fun _ => unit
+  end il :=
+  match As return
+        ∀ (il : ilist As),
+          match As return ilist As → Type with
+            | a :: As' => fun il => B a
+            | [] => fun _ => unit
+          end il with
+    | a :: As => fun il => fst il
+    | [] => fun il => tt
+  end il.
+
+(* Get the cdr of an ilist. *)
+Definition ilist_tl {As : list A} (il : ilist As) :
+  match As return ilist As → Type with
+    | a :: As' => fun il => ilist As'
+    | [] => fun _ => unit
+  end il :=
+  match As return
+        ∀ (il : ilist As),
+          match As return ilist As → Type with
+            | a :: As' => fun il => ilist As'
+            | [] => fun _ => unit
+          end il with
+    | a :: As => fun il => snd il
+    | [] => fun il => tt
+  end il.
+
+Definition ith (n : nat) {As : list A} (il : ilist As)
+  {defA : A} (defB : B defA) : B (nth n As defA).
+Proof.
+  generalize dependent As.
+  induction n; intros.
+  - destruct As; simpl.
+    + exact defB.
+    + exact (fst il).
+  - destruct As; simpl.
+    + exact defB.
+    + apply IHn.
+      exact (snd il).
+Defined.
+
 Equations iapp `(xs : ilist l) `(ys : ilist l') : ilist (l ++ l') :=
   iapp (l:=[]) tt ys := ys;
   iapp (x, xs) ys := (x, iapp xs ys).

Lib/IListVec.v

@@ -1,2 +1,3 @@
+Require Export Category.Solver.Reify.
 Require Export Category.Solver.Normal.
 Require Export Category.Solver.Decide.

Solver.v

@@ -1,8 +1,6 @@
-From Equations Require Import Equations.
-Set Equations With UIP.
-
 Require Import Category.Lib.
 Require Import Category.Theory.Category.
+Require Import Category.Structure.Cartesian.
 Require Import Category.Solver.Expr.
 Require Import Category.Solver.Denote.
 Require Import Category.Solver.Reify.
@@ -12,7 +10,7 @@ Generalizable All Variables.
 
 Section Decide.
 
-Context `{Env}.
+Context `{Arrows}.
 
 (** This code is from Certified Programming with Dependent Types (CPDT). *)
 
@@ -34,89 +32,74 @@ Notation "'Reduce' v" := (if v then Yes else No) (at level 100) : partial_scope.
 Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
 Notation "x && y" := (if x then Reduce y else No) : partial_scope.
 
-Program Fixpoint sexpr_forward (t : SExpr) (hyp : SExpr)
-        (cont : [sexprD t]) :
-  [sexprD hyp → sexprD t] :=
+Program Fixpoint expr_forward (t : Expr) (hyp : Expr)
+        (cont : [exprD t]) :
+  [exprD hyp → exprD t] :=
   match hyp with
-  | STop           => Reduce cont
-  | SBottom        => Yes
-  | SEquiv x y f g => Reduce cont
-  | SAnd p q       => Reduce cont
-  | SOr p q        => if sexpr_forward t p cont
-                      then Reduce (sexpr_forward t q cont)
-                      else No
-  | SImpl _ _      => Reduce cont
+  | Top           => Reduce cont
+  | Bottom        => Yes
+  | Equiv x y f g => Reduce cont
+  | And p q       => Reduce cont
+  | Or p q        => if expr_forward t p cont
+                     then Reduce (expr_forward t q cont)
+                     else No
+  | Impl _ _      => Reduce cont
   end.
 Next Obligation. tauto. Defined.
-Next Obligation. intuition. Defined.
 
-Program Fixpoint sexpr_backward (t : SExpr) {measure t SExpr_subterm} :
-  [sexprD t] :=
+#[local] Obligation Tactic := cat_simpl; intuition.
+
+Program Fixpoint expr_backward (t : Expr) {measure t Expr_subterm} :
+  [exprD t] :=
   match t with
-  | STop => Yes
-  | SBottom => No
-  | SEquiv x y f g => _
-  | SAnd p q       =>
-    match sexpr_backward p with
-    | Proved _ _  => Reduce (sexpr_backward q)
-    | Uncertain _ => No
-    end
-  | SOr p q        =>
-    match sexpr_backward p with
-    | Proved _ _  => Yes
-    | Uncertain _ => Reduce (sexpr_backward q)
-    end
-  | SImpl p q      =>
-    sexpr_forward q p (sexpr_backward q)
+  | Top           => Yes
+  | Bottom        => No
+  | Equiv x y f g => _
+  | And p q       => expr_backward p && expr_backward q
+  | Or p q        => expr_backward p || expr_backward q
+  | Impl p q      => expr_forward q p (expr_backward q)
   end.
 Next Obligation.
-  destruct (list_eqdec _ (sindices f) (sindices g)) eqn:?;
+  destruct (morphism_eq_dec (to_morphism f) (to_morphism g)) eqn:?;
     [|apply Uncertain].
-  destruct (Pos_to_fin _); [|apply Uncertain].
-  destruct (Pos_to_fin _); [|apply Uncertain].
-  destruct (stermD _ _ f) eqn:?; [|apply Uncertain].
-  destruct (stermD _ _ g) eqn:?; [|apply Uncertain].
+  destruct (termD _ _ f) eqn:?; [|apply Uncertain].
+  destruct (termD _ _ g) eqn:?; [|apply Uncertain].
   apply Proved.
-  apply unsindices_sindices_r in Heqo.
-  apply unsindices_sindices_r in Heqo0.
+  apply from_morphism_to_morphism_r in Heqo.
+  apply from_morphism_to_morphism_r in Heqo0.
   rewrite e in Heqo.
   rewrite Heqo in Heqo0.
   now simpl in Heqo0.
 Defined.
-Next Obligation. intuition. Defined.
-Next Obligation. intuition. Defined.
-Next Obligation. intuition. Defined.
-Next Obligation. intuition. Defined.
-Next Obligation. intuition. Defined.
-Next Obligation. apply well_founded_SExpr_subterm. Defined.
+Next Obligation. apply well_founded_Expr_subterm. Defined.
 
-Definition sexpr_tauto : ∀ t, [sexprD t].
-Proof. intros; refine (Reduce (sexpr_backward t)); auto. Defined.
+Definition expr_tauto : ∀ t, [exprD t].
+Proof. intros; refine (Reduce (expr_backward t)); auto. Defined.
 
-Lemma sexpr_sound t :
-  (if sexpr_tauto t then True else False) → sexprD t.
-Proof. unfold sexpr_tauto; destruct t, (sexpr_backward _); tauto. Qed.
+Lemma expr_sound t :
+  (if expr_tauto t then True else False) → exprD t.
+Proof. unfold expr_tauto; destruct t, (expr_backward _); tauto. Qed.
 
 End Decide.
 
 Ltac categorical := reify_terms_and_then
   ltac:(fun env g =>
-          change (@sexprD env g);
-          apply sexpr_sound;
+          change (@exprD env g);
+          apply expr_sound;
           now vm_compute).
 
-Example sample_1 :
-  ∀ (C : Category) (x y z w : C) (f : z ~> w) (g : y ~> z) (h : x ~> y) (i : x ~> z),
-    g ∘ id ∘ id ∘ id ∘ h ≈ i ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
-    g ∘ h ≈ i ->
-    f ∘ (id ∘ g ∘ h) ≈ (f ∘ g) ∘ h.
+Example ex_categorical (C : Category) `{@Cartesian C} (x y z w : C)
+  (f : z ~> w) (g : y ~> z) (h : x ~> y) (i : x ~> z) :
+  g ∘ id ∘ id ∘ id ∘ h ≈ i ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ id ∘ id ∘ id ∘ h ≈ g ∘ h ->
+  g ∘ h ≈ i ->
+  f ∘ (id ∘ g ∘ h) ≈ (f ∘ g) ∘ h.
 Proof.
   intros.
   now categorical.