--- /dev/null
+build/
+build/**
--- /dev/null
+coqc := coqc -noglob
+coqfiles := $(shell find src -name \*.v)
+allfiles := $(coqfiles) $(shell find src -name \*.hs)
+
+default: build/CoqPass.hs
+
+build/CoqPass.hs: build/Makefile.coq $(allfiles)
+
+ # first we build with -dont-load-proofs, since that runs very quickly
+ cd build; make -f Makefile.coq OPT="-dont-load-proofs" Main.vo
+
+ # however the final extraction must be done without -dont-load-proofs
+ cd build; make -f Makefile.coq Extraction.vo
+ cat src/Extraction-prefix.hs build/Extraction.hs > build/CoqPass.hs
+
+build/Makefile.coq: $(coqfiles)
+ mkdir -p build
+ rm -f build/*.v
+ rm -f build/*.d
+ cd build; ln -s ../src/*.v .
+ cd build; coq_makefile *.v > Makefile.coq
+
+clean:
+ rm -rf build
\ No newline at end of file
--- /dev/null
+{-# OPTIONS_GHC -fno-warn-unused-binds #-}
+module Extraction ( coqCoreToStringPass )
+where
+--import HsSyn
+--import TcType
+--import CoreFVs
+--import CoreUtils
+--import MkCore
+--import Var
+--import BasicTypes
+--import Bag
+--import VarSet
+--import SrcLoc
+--import Data.List
+
+import qualified TysWiredIn
+import qualified TysPrim
+import qualified Outputable
+import qualified PrelNames
+import qualified Name
+import qualified Literal
+import qualified Type
+import qualified TypeRep
+import qualified DataCon
+import qualified TyCon
+import qualified Coercion
+import qualified Var
+import qualified Id
+import qualified FastString
+import qualified BasicTypes
+import qualified DataCon
+import qualified CoreSyn
+import qualified Class
+import qualified Data.Char
+
+import Data.Bits ((.&.), shiftL, (.|.))
+import Prelude ( (++), (+), (==), Show, show, Char )
+
+{-
+nat2int :: Nat -> Prelude.Int
+nat2int O = 0
+nat2int (S x) = 1 + (nat2int x)
+
+nat2string :: Nat -> Prelude.String
+nat2string n = show (nat2int n)
+
+-- only needs to sanitize characters which might appear in Haskell identifiers
+sanitizeForLatex :: Prelude.String -> Prelude.String
+sanitizeForLatex [] = []
+sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
+sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
+sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
+sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
+
+coreKindToKind :: TypeRep.Kind -> Kind
+coreKindToKind k =
+ case Coercion.splitKindFunTy_maybe k of
+ Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
+ Prelude.Nothing ->
+ if (Coercion.isLiftedTypeKind k) then KindType
+ else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
+ else if (Coercion.isOpenTypeKind k) then KindOpenType
+ else if (Coercion.isArgTypeKind k) then KindArgType
+ else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
+ else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
+ else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
+ else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
+ (Outputable.showSDoc (Outputable.ppr k)))
+coreVarSort :: Var.Var -> CoreVarSort
+coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v)
+coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v))
+coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v)
+coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
+
+outputableToString :: Outputable -> String
+outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
+-}
--- /dev/null
+(* need this or the Haskell extraction fails *)
+Set Printing Width 1300000.
+
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+Require Import Main.
+Require Import HaskCoreVars.
+Require Import HaskCore.
+
+Open Scope string_scope.
+Extraction Language Haskell.
+
+(* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
+Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive list => "([])" [ "([])" "(:)" ].
+(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
+(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
+Extract Inlined Constant map => "Prelude.map".
+Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
+Extract Inductive prod => "(,)" [ "(,)" ].
+Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
+Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive unit => "()" [ "()" ].
+Extract Inlined Constant string_dec => "(==)".
+Extract Inlined Constant ascii_dec => "(==)".
+Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
+
+(* adapted from ExtrOcamlString.v *)
+Extract Inductive ascii => "Prelude.Char"
+[
+"{- If this appears, you're using Ascii internals. Please don't -} (\ b0 b1 b2 b3 b4 b5 b6 b7 -> let f b i = if b then 1 `shiftL` i else 0 in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))"
+]
+"{- If this appears, you're using Ascii internals. Please don't -} (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
+Extract Constant zero => "'\000'".
+Extract Constant one => "'\001'".
+Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)".
+
+Unset Extraction Optimize.
+Unset Extraction AutoInline.
+
+Definition coqCoreToStringPass (s:CoreExpr CoreVar) : string
+ := "FIXME".
+(*
+Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar
+ :=
+*)
+
+Extraction "Extraction.hs" coqCoreToStringPass.
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* General: general data structures *)
+(*********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Strings.String.
+Require Setoid.
+Require Import Coq.Lists.List.
+Require Import Preamble.
+Generalizable All Variables.
+Require Import Omega.
+
+
+Class EqDecidable (T:Type) :=
+{ eqd_type := T
+; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
+; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _))
+}.
+Coercion eqd_type : EqDecidable >-> Sortclass.
+
+
+(*******************************************************************************)
+(* Trees *)
+
+Inductive Tree (a:Type) : Type :=
+ | T_Leaf : a -> Tree a
+ | T_Branch : Tree a -> Tree a -> Tree a.
+Implicit Arguments T_Leaf [ a ].
+Implicit Arguments T_Branch [ a ].
+
+Notation "a ,, b" := (@T_Branch _ a b) : tree_scope.
+
+(* tree-of-option-of-X comes up a lot, so we give it special notations *)
+Notation "[ q ]" := (@T_Leaf (option _) (Some q)) : tree_scope.
+Notation "[ ]" := (@T_Leaf (option _) None) : tree_scope.
+Notation "[]" := (@T_Leaf (option _) None) : tree_scope.
+
+Open Scope tree_scope.
+
+Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
+ match t with
+ | T_Leaf x => T_Leaf (f x)
+ | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
+ end.
+Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
+ match t with
+ | T_Leaf None => T_Leaf None
+ | T_Leaf (Some x) => T_Leaf (Some (f x))
+ | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
+ end.
+Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
+ match t with
+ | T_Leaf x => f x
+ | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
+ end.
+Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
+ match t with
+ | T_Leaf None => []
+ | T_Leaf (Some x) => f x
+ | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
+ end.
+Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
+ match t with
+ | T_Leaf x => mapLeaf x
+ | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
+ end.
+Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
+ forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
+
+Lemma tree_dec_eq :
+ forall {Q}(t1 t2:Tree ??Q),
+ (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
+ sumbool (t1=t2) (not (t1=t2)).
+ intro Q.
+ intro t1.
+ induction t1; intros.
+
+ destruct a; destruct t2.
+ destruct o.
+ set (X q q0) as X'.
+ inversion X'; subst.
+ left; auto.
+ right; unfold not; intro; apply H. inversion H0; subst. auto.
+ right. unfold not; intro; inversion H.
+ right. unfold not; intro; inversion H.
+ destruct o.
+ right. unfold not; intro; inversion H.
+ left; auto.
+ right. unfold not; intro; inversion H.
+
+ destruct t2.
+ right. unfold not; intro; inversion H.
+ set (IHt1_1 t2_1 X) as X1.
+ set (IHt1_2 t2_2 X) as X2.
+ destruct X1; destruct X2; subst.
+ left; auto.
+
+ right.
+ unfold not; intro H.
+ apply n.
+ inversion H; auto.
+
+ right.
+ unfold not; intro H.
+ apply n.
+ inversion H; auto.
+
+ right.
+ unfold not; intro H.
+ apply n.
+ inversion H; auto.
+ Defined.
+
+
+
+
+(*******************************************************************************)
+(* Lists *)
+
+Notation "a :: b" := (cons a b) : list_scope.
+Open Scope list_scope.
+Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
+ match t with
+ | (T_Leaf l) => match l with
+ | None => nil
+ | Some x => x::nil
+ end
+ | (T_Branch l r) => app (leaves l) (leaves r)
+ end.
+(* weak inverse of "leaves" *)
+Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
+ match l with
+ | nil => []
+ | (a::b) => [a],,(unleaves b)
+ end.
+
+(* a map over a list and the conjunction of the results *)
+Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
+ match l with
+ | nil => True
+ | (a::al) => f a /\ mapProp f al
+ end.
+
+Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
+ induction l.
+ auto.
+ simpl.
+ rewrite IHl.
+ auto.
+ Defined.
+Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
+ intros.
+ induction l; auto.
+ simpl.
+ rewrite IHl.
+ auto.
+ Defined.
+Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
+ (map (g ○ f) l) = (map g (map f l)).
+ intros.
+ induction l.
+ simpl; auto.
+ simpl.
+ rewrite IHl.
+ auto.
+ Defined.
+Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
+ intros.
+ induction b.
+ inversion H.
+ inversion H. apply IHb in H2.
+ auto.
+ Defined.
+Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
+ induction b.
+ intros; inversion H.
+ intros.
+ inversion H.
+ apply IHb in H2.
+ auto.
+ Defined.
+
+Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
+ intros.
+ destruct h.
+ destruct o. inversion H.
+ auto.
+ inversion H.
+ Defined.
+
+Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
+ induction q.
+ destruct a0; simpl.
+ reflexivity.
+ reflexivity.
+ simpl.
+ rewrite IHq1.
+ rewrite IHq2.
+ reflexivity.
+ Qed.
+
+(* handy facts: map preserves the length of a list *)
+Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
+ intros.
+ induction s1.
+ auto.
+ assert False.
+ simpl in H.
+ inversion H.
+ inversion H0.
+ Defined.
+Lemma map_on_singleton : forall A B (f:A->B) x (s1:list A), (cons x nil) = map f s1 -> { y : A & s1=(cons y nil) & (f y)=x }.
+ induction s1.
+ intros.
+ simpl in H; assert False. inversion H. inversion H0.
+ clear IHs1.
+ intros.
+ exists a.
+ simpl in H.
+ assert (s1=nil).
+ inversion H. apply map_on_nil in H2. auto.
+ subst.
+ auto.
+ assert (s1=nil).
+ inversion H. apply map_on_nil in H2. auto.
+ subst.
+ simpl in H.
+ inversion H. auto.
+ Defined.
+
+Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
+ { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
+ intros.
+ destruct s1.
+ inversion H.
+ destruct s1.
+ inversion H.
+ destruct s1.
+ inversion H.
+ exists (a,a0); auto.
+ simpl in H.
+ inversion H.
+ Defined.
+
+
+Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
+ (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
+ induction l.
+ reflexivity.
+ simpl.
+ rewrite IHl1.
+ rewrite IHl2.
+ reflexivity.
+ Defined.
+
+Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
+ (map (g ○ f) l) = (map g (map f l)).
+ intros.
+ induction l.
+ simpl; auto.
+ simpl.
+ rewrite IHl.
+ auto.
+ Defined.
+
+(* sends a::b::c::nil to [[[[],,c],,b],,a] *)
+Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
+ match l with
+ | nil => []
+ | (a::b) => (unleaves' b),,[a]
+ end.
+
+(* sends a::b::c::nil to [[[[],,c],,b],,a] *)
+Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
+ match l with
+ | nil => []
+ | (a::b) => (unleaves'' b),,(T_Leaf a)
+ end.
+
+Fixpoint filter {T:Type}(l:list ??T) : list T :=
+ match l with
+ | nil => nil
+ | (None::b) => filter b
+ | ((Some x)::b) => x::(filter b)
+ end.
+
+Inductive distinct {T:Type} : list T -> Prop :=
+| distinct_nil : distinct nil
+| distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
+
+Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
+ induction l; auto.
+ simpl.
+ omega.
+ Qed.
+
+(* decidable quality on a list of elements which have decidable equality *)
+Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
+ sumbool (eq l1 l2) (not (eq l1 l2)).
+ intro T.
+ intro l1.
+ induction l1; intros.
+ destruct l2.
+ left; reflexivity.
+ right; intro H; inversion H.
+ destruct l2 as [| b l2].
+ right; intro H; inversion H.
+ set (IHl1 l2 dec) as eqx.
+ destruct eqx.
+ subst.
+ set (dec a b) as eqy.
+ destruct eqy.
+ subst.
+ left; reflexivity.
+ right. intro. inversion H. subst. apply n. auto.
+ right.
+ intro.
+ inversion H.
+ apply n.
+ auto.
+ Defined.
+
+
+
+
+(*******************************************************************************)
+(* Length-Indexed Lists *)
+
+Inductive vec (A:Type) : nat -> Type :=
+| vec_nil : vec A 0
+| vec_cons : forall n, A -> vec A n -> vec A (S n).
+
+Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
+ match v with
+ | vec_nil => nil
+ | vec_cons n a va => a::(vec2list va)
+ end.
+
+Require Import Omega.
+Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
+ intro T.
+ intro len.
+ intro v.
+ induction v; intros.
+ assert False.
+ inversion pf.
+ inversion H.
+ rename n into len.
+ destruct n0 as [|n].
+ exact a.
+ apply (IHv n).
+ omega.
+ Defined.
+
+Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
+ induction n.
+ apply vec_nil.
+ inversion va; subst.
+ inversion vb; subst.
+ apply vec_cons; auto.
+ Defined.
+
+Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
+ induction n.
+ apply vec_nil.
+ inversion v; subst.
+ apply vec_cons; auto.
+ Defined.
+
+Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
+ match l with
+ | vec_nil => False
+ | vec_cons _ n m => (n = a) \/ vec_In a m
+ end.
+Implicit Arguments vec_nil [ A ].
+Implicit Arguments vec_cons [ A n ].
+
+Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
+ induction n.
+ apply (vec_cons t vec_nil).
+ apply vec_cons; auto.
+ Defined.
+
+Definition list2vec {T:Type}(l:list T) : vec T (length l).
+ induction l.
+ apply vec_nil.
+ apply vec_cons; auto.
+ Defined.
+
+Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
+ inversion v; auto.
+ Defined.
+Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
+ inversion v; auto.
+ Defined.
+
+Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
+ induction l1.
+ apply vec_nil.
+ apply vec_cons.
+ simpl in *.
+ inversion v; subst; auto.
+ apply IHl1.
+ inversion v; subst; auto.
+ Defined.
+
+Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
+ induction l1.
+ apply v.
+ simpl in *.
+ apply IHl1; clear IHl1.
+ inversion v; subst; auto.
+ Defined.
+
+Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
+
+
+
+(*******************************************************************************)
+(* Shaped Trees *)
+
+(* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
+Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
+| st_nil : @ShapedTree T Q []
+| st_leaf : forall {t}, Q -> @ShapedTree T Q [t]
+| st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
+
+Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
+match st with
+| st_nil => []
+| st_leaf _ q => [q]
+| st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
+end.
+
+Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
+ induction st.
+ apply st_nil.
+ apply st_leaf. apply f. apply q.
+ apply st_branch; auto.
+ Defined.
+
+Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
+ (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
+ induction idx.
+ destruct a.
+ apply st_leaf; auto.
+ inversion st1.
+ inversion st2.
+ auto.
+ apply st_nil.
+ apply st_branch; auto.
+ inversion st1; subst; apply IHidx1; auto.
+ inversion st2; subst; auto.
+ inversion st2; subst; apply IHidx2; auto.
+ inversion st1; subst; auto.
+ Defined.
+
+Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
+ induction idx.
+ destruct a.
+ apply st_leaf; auto.
+ apply st_nil.
+ apply st_branch; auto.
+ Defined.
+
+Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
+ mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
+ intros.
+ induction t; auto.
+ simpl.
+ rewrite IHt1.
+ rewrite IHt2.
+ reflexivity.
+ Qed.
+
+
+
+
+(*******************************************************************************)
+(* Type-Indexed Lists *)
+
+(* an indexed list *)
+Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
+| INil : IList I F nil
+| ICons : forall i is, F i -> IList I F is -> IList I F (i::is).
+Implicit Arguments INil [ I F ].
+Implicit Arguments ICons [ I F ].
+
+(* a tree indexed by a (Tree (option X)) *)
+Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
+| INone : ITree I F []
+| ILeaf : forall i: I, F i -> ITree I F [i]
+| IBranch : forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
+Implicit Arguments INil [ I F ].
+Implicit Arguments ILeaf [ I F ].
+Implicit Arguments IBranch [ I F ].
+
+
+
+
+(*******************************************************************************)
+(* Extensional equality on functions *)
+
+Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
+Hint Transparent extensionality.
+Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
+ intros; apply Build_Equivalence;
+ intros; compute; intros; auto.
+ rewrite H; rewrite H0; auto.
+ Defined.
+ Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
+ with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
+ unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
+ Defined.
+Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
+ (extensionality _ _ f f') ->
+ (extensionality _ _ g g') ->
+ (extensionality _ _ (g ○ f) (g' ○ f')).
+ intros.
+ unfold extensionality.
+ unfold extensionality in H.
+ unfold extensionality in H0.
+ intros.
+ rewrite H.
+ rewrite H0.
+ auto.
+ Qed.
+
+
+
+
+
+
+(* the Error monad *)
+Inductive OrError (T:Type) :=
+| Error : forall error_message:string, OrError T
+| OK : T -> OrError T.
+Notation "??? T" := (OrError T) (at level 10).
+Implicit Arguments Error [T].
+Implicit Arguments OK [T].
+
+Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
+ match oe with
+ | Error s => Error s
+ | OK t => f t
+ end.
+Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
+
+Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
+ match n as N return ???(vec _ N) with
+ | O => match l with
+ | nil => OK vec_nil
+ | _ => Error "list2vecOrError: list was too long"
+ end
+ | S n' => match l with
+ | nil => Error "list2vecOrError: list was too short"
+ | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
+ end
+ end.
+
+Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
+| Indexed_Error : forall error_message:string, Indexed f (Error error_message)
+| Indexed_OK : forall t, f t -> Indexed f (OK t)
+.
+Ltac xauto := try apply Indexed_Error; try apply Indexed_OK.
+
+
+
+
+
+
+(* for a type with decidable equality, we can maintain lists of distinct elements *)
+Section DistinctList.
+ Context `{V:EqDecidable}.
+
+ Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
+ match cvl with
+ | nil => cv::nil
+ | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
+ end.
+
+ Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
+ match cvl with
+ | nil => nil
+ | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
+ end.
+
+ Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
+ match cvrem with
+ | nil => cvl
+ | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
+ end.
+
+ Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
+ match cvl1 with
+ | nil => cvl2
+ | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
+ end.
+End DistinctList.
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskCore: basically GHC's CoreSyn.Expr imported into Coqland *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
+
+(* this type must extract to EXACTLY match TypeRep.Type *)
+Inductive CoreExpr (b:Type) :=
+| CoreEVar : CoreVar -> CoreExpr b
+| CoreELit : HaskLiteral -> CoreExpr b
+| CoreEApp : CoreExpr b -> CoreExpr b -> CoreExpr b
+| CoreELam : b -> CoreExpr b -> CoreExpr b
+| CoreELet : CoreBind b -> CoreExpr b -> CoreExpr b
+| CoreECase : CoreExpr b -> b -> CoreType -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
+| CoreECast : CoreExpr b -> CoreCoercion -> CoreExpr b
+| CoreENote : Note -> CoreExpr b -> CoreExpr b
+| CoreEType : CoreType -> CoreExpr b
+with CoreBind (b:Type) :=
+| CoreNonRec : b -> CoreExpr b -> CoreBind b
+| CoreRec : list (b * CoreExpr b) -> CoreBind b.
+Extract Inductive CoreExpr =>
+ "CoreSyn.Expr" [
+ "CoreSyn.Var"
+ "CoreSyn.Lit"
+ "CoreSyn.App"
+ "CoreSyn.Lam"
+ "CoreSyn.Let"
+ "CoreSyn.Case"
+ "CoreSyn.Cast"
+ "CoreSyn.Note"
+ "CoreSyn.Type" ].
+Extract Inductive CoreBind =>
+ "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
+
+(* extracts the Name from a CoreVar *)
+Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
+
+Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
+ Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
+
+Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *)
+Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ].
+Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ].
+
+(*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*)
+Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType.
+ Extract Inlined Constant mkTyConApp => "Type.mkTyConApp".
+
+(* the magic wired-in name for the modal type introduction form *)
+Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
+
+(* the magic wired-in name for the modal type elimination form *)
+Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
+
+(* detects our crude Core-encoding of modal type introduction/elimination forms *)
+Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
+ | _ => None
+end.
+Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None
+ | _ => None
+end.
+
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskCoreTypes: basically GHC's TypeRep.Type imported into Coqland *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreVars.
+
+Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
+Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)".
+Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
+Instance CoreNameEqDecidable : EqDecidable CoreName :=
+{ eqd_dec := coreName_eq
+; eqd_dec_reflexive := coreName_eq_refl
+}.
+
+Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
+
+(* this exracts onto TypeRep.Type, on the nose *)
+Inductive CoreType :=
+| TyVarTy : CoreVar -> CoreType
+| AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*)
+| TyConApp : forall {n}, TyCon n -> list CoreType -> CoreType
+| FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *)
+| ForAllTy : CoreVar -> CoreType -> CoreType
+| PredTy : PredType -> CoreType
+with PredType :=
+| ClassP : forall {n}, Class_ n -> list CoreType -> PredType
+| IParam : CoreIPName CoreName -> CoreType -> PredType
+| EqPred : CoreType -> CoreType -> PredType.
+Extract Inductive CoreType =>
+ "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
+Extract Inductive PredType =>
+ "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
+
+Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
+
+Definition haskLiteralToCoreType lit : CoreType :=
+ TyConApp (haskLiteralToTyCon lit) nil.
+
+Inductive CoreVarSort : Type :=
+| CoreExprVar : CoreType -> CoreVarSort
+| CoreTypeVar : Kind -> CoreVarSort
+| CoreCoerVar : CoreType * CoreType -> CoreVarSort.
+
+Variable coreVarSort : CoreVar -> CoreVarSort. Extract Inlined Constant coreVarSort => "coreVarSort".
+
+Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString".
+Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString".
+
+Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion".
+Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString".
+Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType.
+ Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskCoreVars: basically GHC's Var.Var imported into Coqland *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import HaskGeneral.
+
+(* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *)
+Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var".
+Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)".
+Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
+Instance CoreVarEqDecidable : EqDecidable CoreVar :=
+{ eqd_dec := coreVar_eq
+; eqd_dec_reflexive := coreVar_eq_refl
+}.
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskGeneral: Definitions shared by all four representations (Core, Weak, Strong, Proof) *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Open Scope nat_scope.
+
+(* all Figure references are to the System FC1 paper *)
+
+(* Figure 1: production T; index is the number of type constructors *)
+Variable TyCon : nat -> Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
+
+(* Figure 1: production "K" *)
+Variable DataCon : ∀n, TyCon n
+ -> nat (* number of existential tyvars associated with this datacon *)
+ -> nat (* number of coercion variables associated with this datacon *)
+ -> nat (* number of value variables (fields) associated with this datacon *)
+ -> Type. Extract Inlined Constant DataCon => "DataCon.DataCon".
+
+Variable CoFunConst : nat -> Type. (* production "C"; extracts to TyCon.TyCon *)
+Variable TyFunConst : nat -> Type. (* production "Sn"; extracts to TyCon.TyCon *)
+
+(* magic TyCons *)
+Variable ArrowTyCon : TyCon 2. (* the TyCon for (->), the regular old function-space type constructor *)
+Variable CoercionTyCon : TyCon 2. (* the TyCon for (+>), the coercion type constructor *)
+Variable hetMetCodeTypeTyCon : TyCon 2. Extract Inlined Constant hetMetCodeTypeTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable Class_ : nat -> Type. Extract Inlined Constant Class_ => "Class.Class".
+Variable classTyCon : ∀ n, Class_ n -> TyCon n. Extract Inlined Constant classTyCon => "Class.classTyCon".
+Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note".
+Implicit Arguments DataCon [ [n] ].
+
+(* Figure 7: production κ, ι *)
+Inductive Kind : Type :=
+ | KindType : Kind (* ★ - the kind of boxed types*)
+ | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *)
+ | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
+ | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
+ | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
+ | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
+
+Notation "'★'" := KindType.
+Notation "a ⇛ b" := (KindTypeFunction a b).
+
+Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString".
+Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString".
+Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString".
+Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring".
+
+
+Axiom tycons_distinct : ~(ArrowTyCon=hetMetCodeTypeTyCon).
+(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
+Variable tyCon_eq : forall {k}(n1 n2:TyCon k), sumbool (n1=n2) (not (n1=n2)).
+ Extract Inlined Constant tyCon_eq => "(==)".
+Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)).
+ Extract Inlined Constant dataCon_eq => "(==)".
+Axiom tyCon_eq_reflexive : forall `(tc:TyCon n), (tyCon_eq tc tc) = (left _ (refl_equal tc)).
+Axiom dataCon_eq_reflexive : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)).
+
+Instance TyConEqDecidable {n} : EqDecidable (TyCon n) :=
+{ eqd_dec := tyCon_eq
+; eqd_dec_reflexive := tyCon_eq_reflexive
+}.
+
+Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) :=
+{ eqd_dec := dataCon_eq
+; eqd_dec_reflexive := dataCon_eq_reflexive
+}.
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskLiterals: representation of compile-time constants (literals) *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import HaskGeneral.
+
+(* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
+Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
+Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
+Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
+Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
+Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
+
+(* This type extracts exactly onto GHC's Literal.Literal type *)
+Inductive HaskLiteral :=
+| HaskMachChar : HaskChar -> HaskLiteral
+| HaskMachStr : HaskFastString -> HaskLiteral
+| HaskMachNullAddr : HaskLiteral
+| HaskMachInt : HaskInteger -> HaskLiteral
+| HaskMachInt64 : HaskInteger -> HaskLiteral
+| HaskMachWord : HaskInteger -> HaskLiteral
+| HaskMachWord64 : HaskInteger -> HaskLiteral
+| HaskMachFloat : HaskRational -> HaskLiteral
+| HaskMachDouble : HaskRational -> HaskLiteral
+| HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral
+with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData.
+
+Extract Inductive HaskLiteral => "Literal.Literal"
+ [ "Literal.MachChar"
+ "Literal.MachStr"
+ "Literal.MachNullAddr"
+ "Literal.MachInt"
+ "Literal.MachInt64"
+ "Literal.MachWord"
+ "Literal.MachWord64"
+ "Literal.MachFloat"
+ "Literal.MachDouble"
+ "Literal.MachLabel" ].
+Extract Inductive HaskFunctionOrData =>
+ "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
+
+(* the TyCons for each of the literals above *)
+Variable addrPrimTyCon : TyCon 0. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
+Variable intPrimTyCon : TyCon 0. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
+Variable wordPrimTyCon : TyCon 0. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
+Variable int64PrimTyCon : TyCon 0. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
+Variable word64PrimTyCon : TyCon 0. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
+Variable floatPrimTyCon : TyCon 0. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
+Variable doublePrimTyCon : TyCon 0. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
+Variable charPrimTyCon : TyCon 0. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
+
+(* retrieves the TyCon for a given Literal *)
+Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 :=
+match lit with
+ | HaskMachNullAddr => addrPrimTyCon
+ | HaskMachChar _ => charPrimTyCon
+ | HaskMachStr _ => addrPrimTyCon
+ | HaskMachInt _ => intPrimTyCon
+ | HaskMachWord _ => wordPrimTyCon
+ | HaskMachInt64 _ => int64PrimTyCon
+ | HaskMachWord64 _ => word64PrimTyCon
+ | HaskMachFloat _ => floatPrimTyCon
+ | HaskMachDouble _ => doublePrimTyCon
+ | HaskMachLabel _ _ _ => addrPrimTyCon
+end.
+
+Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
+
+(* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
+Inductive triple {A B C:Type} :=
+| mkTriple : A -> B -> C -> triple.
+Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
+Extract Inductive triple => "(,,)" [ "(,,)" ].
+
+Inductive AltCon :=
+| DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon
+| LitAlt : HaskLiteral -> AltCon
+| DEFAULT : AltCon.
+Extract Inductive AltCon =>
+ "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskProof: *)
+(* *)
+(* Natural Deduction proofs of the well-typedness of a Haskell term. Proofs use explicit structural rules (Gentzen-style) *)
+(* and are in System FC extended with modal types indexed by Taha-Nielsen environment classifiers (λ^α) *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskStrongTypes.
+
+(* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
+ * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
+ * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
+ * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
+ * types *)
+Inductive Judg :=
+ mkJudg :
+ forall Γ:TypeEnv,
+ forall Δ:CoercionEnv Γ,
+ Tree ??(LeveledHaskType Γ) ->
+ Tree ??(LeveledHaskType Γ) ->
+ Judg.
+ Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
+
+(* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
+ * uniform context throughout the whole proof. Such proofs are important because (1) we can do left and right context
+ * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
+Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
+ mkUJudg :
+ Tree ??(LeveledHaskType Γ) ->
+ Tree ??(LeveledHaskType Γ) ->
+ UJudg Γ Δ.
+ Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
+ Notation "'ext_tree_left'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t) s end).
+ Notation "'ext_tree_right'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end).
+
+(* we can turn a UJudg into a Judg by simply internalizing the index *)
+Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
+ match ej with mkUJudg t s => Γ > Δ > t |- s end.
+ Coercion UJudg2judg : UJudg >-> Judg.
+
+(* information needed to define a case branch in a HaskProof *)
+Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} :=
+{ cbi_cbi : @StrongAltConInContext n tc Γ avars
+; cbri_freevars : Tree ??(LeveledHaskType Γ)
+; cbri_judg := cbi_Γ cbi_cbi > cbi_Δ cbi_cbi
+ > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi)))
+ |- [weakLT' (branchtype @@ lev)]
+}.
+Implicit Arguments ProofCaseBranch [ ].
+
+(* Figure 3, production $\vdash_E$, Uniform rules *)
+Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
+| RCanL : ∀ t a , URule [Γ>>Δ> [],,a |- t ] [Γ>>Δ> a |- t ]
+| RCanR : ∀ t a , URule [Γ>>Δ> a,,[] |- t ] [Γ>>Δ> a |- t ]
+| RuCanL : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> [],,a |- t ]
+| RuCanR : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> a,,[] |- t ]
+| RAssoc : ∀ t a b c , URule [Γ>>Δ>a,,(b,,c) |- t ] [Γ>>Δ>(a,,b),,c |- t ]
+| RCossa : ∀ t a b c , URule [Γ>>Δ>(a,,b),,c |- t ] [Γ>>Δ> a,,(b,,c) |- t ]
+| RLeft : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
+| RRight : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
+| RExch : ∀ t a b , URule [Γ>>Δ> (b,,a) |- t ] [Γ>>Δ> (a,,b) |- t ]
+| RWeak : ∀ t a , URule [Γ>>Δ> [] |- t ] [Γ>>Δ> a |- t ]
+| RCont : ∀ t a , URule [Γ>>Δ> (a,,a) |- t ] [Γ>>Δ> a |- t ].
+
+
+(* Figure 3, production $\vdash_E$, all rules *)
+Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
+
+| RURule : ∀ Γ Δ h c, @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
+
+(* λ^α rules *)
+| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]]
+| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]]
+
+(* Part of GHC, but not explicitly in System FC *)
+| RNote : ∀ h c, Note -> Rule h [ c ]
+| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]]
+
+(* SystemFC rules *)
+| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
+| RLam : ∀ Γ Δ Σ tx te l, Γ ⊢ᴛy tx : ★ -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
+| RCast : ∀ Γ Δ Σ σ τ γ l, Δ ⊢ᴄᴏ γ : σ ∼ τ -> Rule [Γ>Δ> Σ |- [σ@@l] ] [Γ>Δ> Σ |- [τ @@l]]
+| RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
+| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
+| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
+| REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
+| RAppT : ∀ Γ Δ Σ κ σ τ l, Γ ⊢ᴛy τ : κ -> Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
+| RAbsT : ∀ Γ Δ Σ κ σ l,
+ Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
+ [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
+| RAppCo : forall Γ Δ Σ κ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ ->
+ Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
+| RAbsCo : ∀ Γ Δ Σ κ σ σ₁ σ₂ l,
+ Γ ⊢ᴛy σ₁:κ ->
+ Γ ⊢ᴛy σ₂:κ ->
+ Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
+ [Γ > Δ > Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]]
+| RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
+| RCase : forall Γ Δ lev n tc Σ avars tbranches
+ (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)),
+ Rule
+ ((mapOptionTree cbri_judg alts),,
+ [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ])
+ [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches @@ lev ] ]
+.
+Coercion RURule : URule >-> Rule.
+
+
+(* A rule is considered "flat" if it is neither RBrak nor REsc *)
+Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
+| Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r)
+| Flat_RNote : ∀ x y z , Rule_Flat (RNote x y z)
+| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
+| Flat_RLam : ∀ Γ Δ Σ tx te q l, Rule_Flat (RLam Γ Δ Σ tx te q l)
+| Flat_RCast : ∀ Γ Δ Σ σ τ γ q l, Rule_Flat (RCast Γ Δ Σ σ τ γ q l)
+| Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
+| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q l, Rule_Flat (RAppT Γ Δ Σ κ σ τ q l)
+| Flat_RAppCo : ∀ Γ Δ Σ κ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ q l)
+| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x )
+| Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
+| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
+| Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e)
+| Flat_RCase : ∀ Σ Γ T κlen κ θ l x q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q).
+
+(* given a proof that uses only uniform rules, we can produce a general proof *)
+Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
+ := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
+
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskStrong: a dependently-typed version of CoreSyn *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskStrongTypes.
+
+Section HaskStrong.
+
+ (* any type with decidable equality may be used to represent value variables *)
+ Context `{EQD_VV:EqDecidable VV}.
+
+ (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *)
+ Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
+ { cbi_sacic : @StrongAltConInContext n tc Γ atypes
+ ; cbi_vars : vec VV (tagNumValVars (cbi_tag cbi_sacic))
+ ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic))
+ }.
+ Implicit Arguments ExprCaseBranch [[n][Γ]].
+ Coercion cbi_sacic : ExprCaseBranch >-> StrongAltConInContext.
+
+ Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type :=
+ | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
+ | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
+ | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
+ | ELam : ∀ Γ Δ ξ t1 t2 l ev, Γ ⊢ᴛy t1:★ ->Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
+ | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
+ | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l))
+ | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
+ | ECast : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 -> Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l)
+ | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t
+ | ETyApp : ∀ Γ Δ κ σ τ ξ l, Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l)
+ | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ :κ ⇒ σ @@ l)
+ | ECoApp : ∀ Γ Δ κ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ : κ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l)
+ | ETyLam : ∀ Γ Δ ξ κ σ l,
+ Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
+
+ | ECase : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches,
+ Expr Γ Δ ξ (caseType tc atypes @@ l) ->
+ Tree ??{ scb : ExprCaseBranch tc atypes
+ & Expr (cbi_Γ scb) (cbi_Δ scb) (update_ξ (weakLT'○ξ) (cbi_varstypes scb)) (weakLT' (tbranches@@l)) } ->
+ Expr Γ Δ ξ (tbranches @@ l)
+
+ | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
+ ELetRecBindings Γ Δ ξ' l (mapOptionTree (@snd _ _) vars) ->
+ Expr Γ Δ ξ' (τ@@l) ->
+ Expr Γ Δ ξ (τ@@l)
+
+ (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *)
+ with ELetRecBindings : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(HaskType Γ) -> Type :=
+ | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l []
+ | ELR_leaf : ∀ Γ Δ ξ t l, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [t]
+ | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
+ .
+
+End HaskStrong.
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskStrongTypes: representation of types and coercions for HaskStrong *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+
+(* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
+Section Raw.
+
+ (* TV is the PHOAS type which stands for type variables of System FC *)
+ Context {TV:Type}.
+
+ (* Figure 7: ρ, σ, τ, ν *)
+ Inductive RawHaskType : Type :=
+ | TVar : TV -> RawHaskType (* a *)
+ | TCon : ∀n, TyCon n -> RawHaskType (* T *)
+ | TCoerc : Kind -> RawHaskType (* (+>) *)
+ | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *)
+ | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *)
+ | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *)
+ | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *).
+
+ (* the "kind" of a coercion is a pair of types *)
+ Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
+
+ Section CV.
+
+ (* the PHOAS type which stands for coercion variables of System FC *)
+ Context {CV:Type}.
+
+ (* Figure 7: γ, δ *)
+ Inductive RawHaskCoer : Prop :=
+ | CoVar : CV -> RawHaskCoer (* g *)
+ | CoType : RawHaskType -> RawHaskCoer (* τ *)
+ | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
+ | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
+ | CoCFApp : ∀n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
+ | CoTFApp : ∀n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
+ | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
+ | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
+ | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
+ | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
+ | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
+
+ End CV.
+End Raw.
+
+Implicit Arguments TCon [ [TV] [n]].
+Implicit Arguments TFCApp [ [TV] [n]].
+Implicit Arguments RawHaskType [ ].
+Implicit Arguments RawHaskCoer [ ].
+Implicit Arguments RawCoercionKind [ ].
+
+Notation "t1 ---> t2" := (fun TV env => (@TApp _ (@TApp _ (@TCon TV _ ArrowTyCon) (t1 TV env)) (t2 TV env))).
+Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" :=
+ (fun TV env => @TApp _ (@TApp _ (@TCon _ _ ArrowTyCon) (@TApp _ (@TApp _ (@TCoerc _ κ) (φ₁ TV env)) (φ₂ TV env))) (φ₃ TV env)).
+
+
+
+(* Kind and Coercion Environments *)
+(*
+ * In System FC, the environment consists of three components, each of
+ * whose well-formedness depends on all of those prior to it:
+ *
+ * 1. (TypeEnv) The list of free type variables and their kinds
+ * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
+ * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
+ *)
+
+Definition TypeEnv := list Kind.
+Definition InstantiatedTypeEnv (TV:Type) (Γ:TypeEnv) := vec TV (length Γ).
+Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
+Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
+Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
+
+
+(* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
+Definition HaskTyVar (Γ:TypeEnv) := forall TV (env:@InstantiatedTypeEnv TV Γ), TV.
+Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
+Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ).
+Definition HaskType (Γ:TypeEnv) := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV.
+Definition HaskCoercion Γ Δ := ∀ TV CV,
+ @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV.
+Inductive LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ.
+Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) := fun TV env => vec_head env.
+Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : HaskType Γ
+ := fun TV env => TAll κ (σ TV env).
+Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ
+ := fun TV env => σ TV env (cv TV env).
+Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
+Definition HaskTCon {Γ}{n}(tc:TyCon n) : HaskType Γ := fun TV ite => TCon tc.
+Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite).
+Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ :=
+ fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite).
+
+
+(* PHOAS substitution on types *)
+Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
+ := fun TV env =>
+ (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
+ match exp with
+ | TVar x => x
+ | TAll k y => TAll k (fun v => flattenT (y (TVar v)))
+ | TApp x y => TApp (flattenT x) (flattenT y)
+ | TCon n tc => TCon tc
+ | TCoerc k => TCoerc k
+ | TCode v e => TCode (flattenT v) (flattenT e)
+ | TFCApp n tfc lt => TFCApp tfc
+ ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n :=
+ match expv in vec _ N return vec (RawHaskType TV) N with
+ | vec_nil => vec_nil
+ | x:::y => (flattenT x):::(flatten_vec _ y)
+ end) n lt)
+ end)
+ (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)).
+Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20).
+Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
+Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
+
+
+
+
+(* A "tag" is something that distinguishes one case branch from another; it's a lot like Core's AltCon *)
+Inductive Tag {n:nat}(tc:TyCon n) : Type :=
+| TagDefault : Tag tc
+| TagLiteral : forall lit:HaskLiteral , Tag tc (* FIXME: solution is a new StrongLiteral indexed by a tycon *)
+| TagDataCon : forall m q z, DataCon tc m q z -> Tag tc.
+
+(* the number of value variables bound in branches with the given tag *)
+Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
+ match tag with
+ | TagDefault => 0
+ | TagLiteral lit => 0
+ | TagDataCon m q z dc => z
+ end.
+
+(* the number of existential type variables bound in branches with the given tag *)
+Definition tagNumExVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
+ match tag with
+ | TagDefault => 0
+ | TagLiteral lit => 0
+ | TagDataCon m q z dc => m
+ end.
+
+(* the number of coercion variables bound in branches with the given tag *)
+Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
+ match tag with
+ | TagDefault => 0
+ | TagLiteral lit => 0
+ | TagDataCon m q z dc => q
+ end.
+
+Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) :=
+ fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
+
+Record StrongAltCon {n}{tc:TyCon n}{alt:Tag tc} :=
+{ cb_akinds : vec Kind n
+; cb_ekinds : vec Kind (tagNumExVars alt)
+; cb_kinds := app (vec2list cb_akinds) (vec2list cb_ekinds)
+; cb_coercions : vec (HaskType cb_kinds * HaskType cb_kinds) (tagNumCoVars alt)
+; cb_types : vec (HaskType cb_kinds) (tagNumValVars alt)
+}.
+Implicit Arguments StrongAltCon [[n][tc]].
+
+
+
+
+
+
+
+
+
+
+(* FIXME: it's a mess below this point *)
+
+
+Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite.
+Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
+ map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
+Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind)
+ : InstantiatedTypeEnv TV (κ::Γ) := tv:::env.
+Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind)
+ : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
+ simpl.
+ unfold InstantiatedCoercionEnv.
+ unfold addKindToCoercionEnv.
+ simpl.
+ rewrite <- map_preserves_length.
+ apply env.
+ Defined.
+Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop
+ := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)).
+Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ)
+ (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
+ := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
+Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
+ κ::Δ.
+Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
+ : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
+ simpl.
+ unfold addCoercionToCoercionEnv; simpl.
+ unfold InstantiatedCoercionEnv; simpl.
+ apply vec_cons; auto.
+ Defined.
+Notation "env ∋ tv : κ" := (@typeEnvContainsType _ _ env tv κ).
+Notation "env '+' tv : κ" := (@addKindToInstantiatedTypeEnv _ _ env tv κ).
+
+(* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
+Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite.
+Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
+ induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
+Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
+Definition weakV {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)).
+Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ).
+ induction κ; auto. apply weakV; auto. Defined.
+Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite).
+Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
+Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ).
+ induction κ; auto. apply weakT; auto. Defined.
+Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ).
+unfold HaskType in *.
+unfold InstantiatedTypeEnv in *.
+intros.
+apply vec_chop in X.
+apply lt.
+apply X.
+Defined.
+Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (app b c)).
+rewrite <- ass_app in lt.
+exact lt.
+Defined.
+Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
+ induction κ; auto. apply weakL; auto. Defined.
+Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end.
+Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ)
+ := match lt with t @@ l => weakT' t @@ weakL' l end.
+Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
+ induction κ; auto. apply weakCE; auto. Defined.
+Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
+ : InstantiatedCoercionEnv TV CV Γ Δ.
+ intros.
+ unfold InstantiatedCoercionEnv; intros.
+ unfold InstantiatedCoercionEnv in ice.
+ unfold weakCE in ice.
+ simpl in ice.
+ rewrite <- map_preserves_length in ice.
+ apply ice.
+ Defined.
+Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ))
+ : InstantiatedCoercionEnv TV CV Γ Δ.
+ induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined.
+Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
+ fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
+Definition weakC {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) :=
+ fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice).
+Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) :
+ forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV
+ := fun TV ite tv => (f TV (weakITE ite) tv).
+
+(***************************************************************************************************)
+(* Well-Formedness of Types and Coercions *)
+(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
+Inductive TypeFunctionDecl (n:nat)(tfc:TyFunConst n)(vk:vec Kind n) : Type :=
+ mkTFD : Kind -> TypeFunctionDecl n tfc vk.
+
+
+(* Figure 8, upper half *)
+Inductive WellKinded_RawHaskType (TV:Type)
+ : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop :=
+ | WFTyVar : forall Γ env κ d,
+ env∋d:κ ->
+ WellKinded_RawHaskType TV Γ env (TVar d) κ
+ | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂,
+ WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) ->
+ WellKinded_RawHaskType TV Γ env σ₂ κ₂ ->
+ WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂
+ | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ ,
+ (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) ->
+ WellKinded_RawHaskType TV _ env (TAll κ σ) ★
+ | TySCon : forall Γ env n tfc lt vk ι ,
+ @TypeFunctionDecl n tfc vk ->
+ ListWellKinded_RawHaskType TV Γ _ env lt vk ->
+ WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι
+with ListWellKinded_RawHaskType (TV:Type)
+ : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop :=
+ | ListWFRawHaskTypenil : forall Γ env,
+ ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil
+ | ListWFRawHaskTypecons : forall Γ env n t k lt lk,
+ WellKinded_RawHaskType TV Γ env t k ->
+ ListWellKinded_RawHaskType TV Γ n env lt lk ->
+ ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk).
+
+(*
+Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind :=
+match rht with
+ | TVar k => k
+ | TCon n tc => ̱★ (* FIXME: use the StrongAltCon *)
+ | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ ))
+ | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *)
+ | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *)
+ | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *)
+ | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *).
+*)
+Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
+ forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
+ Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
+
+
+
+(* "decl", production for "axiom" *)
+Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type :=
+{ axd_τ : vec TV n -> RawHaskType TV
+; axd_σ : vec TV n -> RawHaskType TV
+}.
+
+
+
+
+Section WFCo.
+ Context {TV:Type}.
+ Context {CV:Type}.
+
+ (* local notations *)
+ Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
+ Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
+ (at level 20, t1 at level 99, t2 at level 99, t at level 99).
+ Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
+ (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
+
+ (* Figure 8, lower half *)
+ Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
+ @InstantiatedTypeEnv TV Γ ->
+ @InstantiatedCoercionEnv TV CV Γ Δ ->
+ @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=.
+(*
+ | CoTVar':∀ Γ Δ t e c σ τ,
+ (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
+ | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
+ | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
+ | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
+ | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
+ | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
+ | SComp :∀ Γ Δ t e γ n S σ τ κ,
+ ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t
+ | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
+ ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
+ ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
+ ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
+ e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
+
+ | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
+ (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
+ -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
+
+ | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
+ (t ⊢ᴛy TApp σ₁ σ₂:κ)->
+ (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
+ (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
+ e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
+
+ | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
+ t ⊢ᴛy v TV t : κ ->
+ (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
+ e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
+ with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
+ @InstantiatedTypeEnv TV Γ ->
+ InstantiatedCoercionEnv TV CV Γ Δ ->
+ list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
+ | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
+ | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
+ ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
+ where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
+*)
+End WFCo.
+
+Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
+ forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
+ @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
+ Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
+
+ Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
+ Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
+
+
+Fixpoint update_ξ
+ `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
+ match vt with
+ | nil => ξ
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+ end.
+
+
+
+
+
+
+
+
+
+
+
+(*
+Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)).
+Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
+Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end.
+(* the type of the scrutinee in a case branch *)
+Require Import Coq.Arith.EqNat.
+Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}.
+ intros.
+ destruct H.
+ exists x; omega.
+ Defined.
+Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n.
+ induction n.
+ apply vec_nil.
+ apply vec_cons.
+ exists n; omega.
+ apply (vec_map (bump _)); auto.
+ Defined.
+Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)).
+ set (hv1 _ (vecOfNats _)) as hv1'.
+ set (hv2 _ (vecOfNats _)) as hv2'.
+ destruct hv1' as [hv1_n hv1_pf].
+ destruct hv2' as [hv2_n hv2_pf].
+ clear hv1_pf.
+ clear hv2_pf.
+ set (eq_nat_decide hv1_n hv2_n) as dec.
+ destruct dec.
+ left. admit.
+ right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl.
+ Defined.
+(* equality on levels is decidable *)
+Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2))
+ := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2.
+*)
+
+
+
+
+
+(* just like GHC's AltCon, but using PHOAS types and coercions *)
+Record StrongAltConInContext {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
+{ cbi_tag : Tag tc
+; cbi_cb : StrongAltCon cbi_tag
+; cbi_Γ : TypeEnv := app (vec2list (cb_ekinds cbi_cb)) Γ
+; cbi_Δ : CoercionEnv cbi_Γ
+; cbi_types : vec (LeveledHaskType (app (vec2list (cb_ekinds cbi_cb)) Γ)) (tagNumValVars cbi_tag)
+}.
+Implicit Arguments StrongAltConInContext [[n][Γ]].
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskWeak: a non-dependently-typed but Coq-friendly version of HaskCore *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+
+Inductive WeakExpr :=
+| WEVar : CoreVar -> WeakExpr
+| WELit : HaskLiteral -> WeakExpr
+| WELet : CoreVar -> WeakExpr -> WeakExpr -> WeakExpr
+| WELetRec : Tree ??(CoreVar * WeakExpr) -> WeakExpr -> WeakExpr
+| WECast : WeakExpr -> CoreCoercion -> WeakExpr
+| WENote : Note -> WeakExpr -> WeakExpr
+| WEApp : WeakExpr -> WeakExpr -> WeakExpr
+| WETyApp : WeakExpr -> CoreType -> WeakExpr
+| WECoApp : WeakExpr -> CoreCoercion -> WeakExpr
+| WELam : CoreVar -> WeakExpr -> WeakExpr
+| WETyLam : CoreVar -> WeakExpr -> WeakExpr
+| WECoLam : CoreVar -> WeakExpr -> WeakExpr
+| WEBrak : CoreVar -> WeakExpr -> WeakExpr
+| WEEsc : CoreVar -> WeakExpr -> WeakExpr
+| WECase : forall (scrutinee:WeakExpr)
+ (tbranches:CoreType)
+ {n:nat}(tc:TyCon n)
+ (type_params:vec CoreType n)
+ (alts : Tree ??(AltCon*list CoreVar*WeakExpr)),
+ WeakExpr.
+
+(* calculate the free CoreVar's in a WeakExpr *)
+Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
+ match me with
+ | WELit _ => nil
+ | WEVar cv => cv::nil
+ | WECast e co => getWeakExprFreeVars e
+ | WENote n e => getWeakExprFreeVars e
+ | WETyApp e t => getWeakExprFreeVars e
+ | WECoApp e co => getWeakExprFreeVars e
+ | WEBrak ec e => getWeakExprFreeVars e
+ | WEEsc ec e => getWeakExprFreeVars e
+ | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
+ | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2)
+ | WELam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
+ | WETyLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
+ | WECoLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
+
+ (* the messy fixpoints below are required by Coq's termination conditions *)
+ | WECase scrutinee tbranches n tc type_params alts =>
+ mergeDistinctLists (getWeakExprFreeVars scrutinee) (
+ ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list CoreVar*WeakExpr)) {struct alts} : list CoreVar :=
+ match alts with
+ | T_Leaf None => nil
+ | T_Leaf (Some (DEFAULT,_,e)) => getWeakExprFreeVars e
+ | T_Leaf (Some (LitAlt lit,_,e)) => getWeakExprFreeVars e
+ | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e)) => removeFromDistinctList' vars (getWeakExprFreeVars e)
+ | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
+ end) alts))
+ | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) :=
+ match mlr with
+ | T_Leaf None => cvl
+ | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
+ | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
+ end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
+ ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) :=
+ match mlr with
+ | T_Leaf None => nil
+ | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
+ | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
+ end) mlr))
+ end.
+
+(* wrap lambdas around an expression until it has no free variables *)
+Definition makeClosedExpression : WeakExpr -> WeakExpr :=
+ fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) :=
+ match cvl with
+ | nil => me
+ | cv::cvl' => WELam cv (closeExpression me cvl')
+ end) me (getWeakExprFreeVars me).
+
+(* messy first-order capture-avoiding substitution on CoreType's *)
+Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) :=
+ match te with
+ | TyVarTy tv' => if eqd_dec tv tv' then tsubst else te
+ | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
+ | FunTy t1 t2 => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
+ | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
+ | PredTy (EqPred t1 t2) => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
+ | PredTy (IParam ip ty) => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
+ | PredTy (ClassP _ c lt) => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
+ match lt with
+ | nil => nil
+ | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
+ end) lt))
+ | TyConApp _ tc lt => TyConApp tc ((fix replaceCoreDistinctList (lt:list CoreType) :=
+ match lt with
+ | nil => nil
+ | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
+ end) lt)
+ end.
+
+(* calculate the CoreType of a WeakExpr *)
+Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
+ match ce with
+ | WEVar v => match coreVarSort v with
+ | CoreExprVar t => OK t
+ | CoreTypeVar _ => Error "found tyvar in expression"
+ | CoreCoerVar _ => Error "found coercion variable in expression"
+ end
+ | WELit lit => OK (haskLiteralToCoreType lit)
+ | WEApp e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
+ match t' with
+ | FunTy t1 t2 => OK t2
+ | (TyConApp 2 tc (t1::t2::nil)) =>
+ if (tyCon_eq tc ArrowTyCon)
+ then OK t2
+ else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
+ | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
+ end
+ | WETyApp e t => coreTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | ForAllTy v ct => match coreVarSort v with
+ | CoreExprVar _ => Error "found an expression variable inside an forall-type!"
+ | CoreTypeVar _ => OK (replaceCoreVar ct v t)
+ | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!"
+ end
+ | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp")
+ end
+ | WECoApp e co => coreTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3
+ | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
+ if (tyCon_eq tc ArrowTyCon)
+ then OK t3
+ else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
+ | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
+ end
+ | WELam ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with
+ | CoreExprVar vt => OK (FunTy vt t')
+ | CoreTypeVar _ => Error "found a type variable in a WELam!"
+ | CoreCoerVar _ => Error "found a coercion variable in a WELam!"
+ end
+ | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t')
+ | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with
+ | CoreExprVar vt => Error "found an expression variable in a WECoLam!"
+ | CoreTypeVar _ => Error "found a type variable in a WECoLam!"
+ | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t')
+ end
+ | WELet ev ve e => coreTypeOfWeakExpr e
+ | WELetRec rb e => coreTypeOfWeakExpr e
+ | WENote n e => coreTypeOfWeakExpr e
+ | WECast e co => OK (snd (coreCoercionKind co))
+ | WECase scrutinee tbranches n tc type_params alts => OK tbranches
+ | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil))
+ | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' =>
+ match t' with
+ | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
+ if (tyCon_eq tc hetMetCodeTypeTyCon)
+ then if eqd_dec ec ec' then OK t''
+ else Error "level mismatch in escapification"
+ else Error "ill-typed escapification"
+ | _ => Error "ill-typed escapification"
+ end
+ end.
+
--- /dev/null
+Require Import Preamble.
+Require Import General.
+
+Require Import NaturalDeduction.
+Require Import NaturalDeductionToLatex.
+
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+Require Import HaskCore.
+Require Import HaskWeak.
+(*Require Import HaskCoreToWeak.*)
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+(*Require Import HaskStrongToProof.*)
+Require Import HaskProof.
+(*Require Import HaskWeakToStrong.*)
+(*Require Import HaskProofToLatex.*)
--- /dev/null
+(*********************************************************************************************************************************)
+(* NaturalDeduction: structurally explicit proofs in Coq *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+
+(*
+ * IMPORTANT!!!
+ *
+ * Unlike most formalizations, this library offers TWO different ways
+ * to represent a natural deduction proof. To demonstrate this,
+ * consider the signature of the propositional calculus:
+ *
+ * Variable PropositionalVariable : Type.
+ *
+ * Inductive Formula : Prop :=
+ * | formula_var : PropositionalVariable -> Formula (* every propositional variable is a formula *)
+ * | formula_and : Formula -> Formula -> Formula (* the conjunction of any two formulae is a formula *)
+ * | formula_or : Formula -> Formula -> Formula (* the disjunction of any two formulae is a formula *)
+ *
+ * And couple this with the theory of conjunction and disjunction:
+ * φ\/ψ is true if either φ is true or ψ is true, and φ/\ψ is true
+ * if both φ and ψ are true.
+ *
+ * 1) Structurally implicit proofs
+ *
+ * This is what you would call the "usual" representation –- it's
+ * what most people learn when they first start programming in Coq:
+ *
+ * Inductive IsTrue : Formula -> Prop :=
+ * | IsTrue_or1 : forall f1 f2, IsTrue f1 -> IsTrue (formula_or f1 f2)
+ * | IsTrue_or2 : forall f1 f2, IsTrue f2 -> IsTrue (formula_or f1 f2)
+ * | IsTrue_and : forall f1 f2, IsTrue f2 -> IsTrue f2 -> IsTrue (formula_and f1 f2)
+ *
+ * Here each judgment (such as "φ is true") is represented by a Coq
+ * type; furthermore:
+ *
+ * 1. A proof of a judgment is any inhabitant of that Coq type.
+ *
+ * 2. A proof of a judgment "J2" from hypothesis judgment "J1"
+ * is any Coq function from the Coq type for J1 to the Coq
+ * type for J2; Composition of (hypothetical) proofs is
+ * represented by composition of Coq functions.
+ *
+ * 3. A pair of judgments is represented by their product (Coq
+ * type [prod]) in Coq; a pair of proofs is represented by
+ * their pair (Coq function [pair]) in Coq.
+ *
+ * 4. Duplication of hypotheses is represented by the Coq
+ * function (fun x => (x,x)). Dereliction of hypotheses is
+ * represented by the coq function (fun (x,y) => x) or (fun
+ * (x,y) => y). Exchange of the order of hypotheses is
+ * represented by the Coq function (fun (x,y) => (y,x)).
+ *
+ * The above can be done using lists instead of tuples.
+ *
+ * The advantage of this approach is that it requires a minimum
+ * amount of syntax, and takes maximum advantage of Coq's
+ * automation facilities.
+ *
+ * The disadvantage is that one cannot reason about proof-theoretic
+ * properties *generically* across different signatures and
+ * theories. Each signature has its own type of judgments, and
+ * each theory has its own type of proofs. In the present
+ * development we will want to prove –– in this generic manner --
+ * that various classes of natural deduction calculi form various
+ * kinds of categories. So we will need this ability to reason
+ * about proofs independently of the type used to represent
+ * judgments and (more importantly) of the set of basic inference
+ * rules.
+ *
+ * 2) Structurally explicit proofs
+ *
+ * Structurally explicit proofs are formalized in this file
+ * (NaturalDeduction.v) and are designed specifically in order to
+ * circumvent the problem in the previous paragraph.
+ *
+ *)
+
+(*
+ * REGARDING LISTS versus TREES:
+ *
+ * You'll notice that this formalization uses (Tree (option A)) in a
+ * lot of places where you might find (list A) more natural. If this
+ * bothers you, see the end of the file for the technical reasons why.
+ * In short, it lets us avoid having to mess about with JMEq or EqDep,
+ * which are not as well-supported by the Coq core as the theory of
+ * CiC proper.
+ *)
+
+Section Natural_Deduction.
+
+ (* any Coq Type may be used as the set of judgments *)
+ Context {Judgment : Type}.
+
+ (* any Coq Type –- indexed by the hypothesis and conclusion judgments -- may be used as the set of basic inference rules *)
+ Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
+
+ (*
+ * This type represents a valid Natural Deduction proof from a list
+ * (tree) of hypotheses; the notation H/⋯⋯/C is meant to look like
+ * a proof tree with the middle missing if you tilt your head to
+ * the left (yeah, I know it's a stretch). Note also that this
+ * type is capable of representing proofs with multiple
+ * conclusions, whereas a Rule may have only one conclusion.
+ *)
+ Inductive ND :
+ forall hypotheses:Tree ??Judgment,
+ forall conclusions:Tree ??Judgment,
+ Type :=
+
+ (* natural deduction: you may infer anything from itself -- "identity proof" *)
+ | nd_id0 : [ ] /⋯⋯/ [ ]
+ | nd_id1 : forall h, [ h ] /⋯⋯/ [ h ]
+
+ (* natural deduction: you may discard conclusions *)
+ | nd_weak : forall h, [ h ] /⋯⋯/ [ ]
+
+ (* natural deduction: you may duplicate conclusions *)
+ | nd_copy : forall h, h /⋯⋯/ (h,,h)
+
+ (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
+ | nd_prod : forall {h1 h2 c1 c2}
+ (pf1: h1 /⋯⋯/ c1 )
+ (pf2: h2 /⋯⋯/ c2),
+ ( h1 ,, h2 /⋯⋯/ c1 ,, c2)
+
+ (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
+ | nd_comp :
+ forall {h x c}
+ `(pf1: h /⋯⋯/ x)
+ `(pf2: x /⋯⋯/ c),
+ ( h /⋯⋯/ c)
+
+ (* structural rules on lists of judgments *)
+ | nd_cancell : forall {a}, [] ,, a /⋯⋯/ a
+ | nd_cancelr : forall {a}, a ,, [] /⋯⋯/ a
+ | nd_llecnac : forall {a}, a /⋯⋯/ [] ,, a
+ | nd_rlecnac : forall {a}, a /⋯⋯/ a ,, []
+ | nd_assoc : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c)
+ | nd_cossa : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c
+
+ (* any Rule by itself counts as a proof *)
+ | nd_rule : forall {h c} (r:Rule h c), h /⋯⋯/ c
+
+ where "H /⋯⋯/ C" := (ND H C).
+
+ Notation "H /⋯⋯/ C" := (ND H C) : pf_scope.
+ Notation "a ;; b" := (nd_comp a b) : nd_scope.
+ Notation "a ** b" := (nd_prod a b) : nd_scope.
+ Open Scope nd_scope.
+ Open Scope pf_scope.
+
+ (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
+ Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
+ | nd_structural_id0 : Structural nd_id0
+ | nd_structural_id1 : forall h, Structural (nd_id1 h)
+ | nd_structural_weak : forall h, Structural (nd_weak h)
+ | nd_structural_copy : forall h, Structural (nd_copy h)
+ | nd_structural_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
+ | nd_structural_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
+ | nd_structural_cancell : forall {a}, Structural (@nd_cancell a)
+ | nd_structural_cancelr : forall {a}, Structural (@nd_cancelr a)
+ | nd_structural_llecnac : forall {a}, Structural (@nd_llecnac a)
+ | nd_structural_rlecnac : forall {a}, Structural (@nd_rlecnac a)
+ | nd_structural_assoc : forall {a b c}, Structural (@nd_assoc a b c)
+ | nd_structural_cossa : forall {a b c}, Structural (@nd_cossa a b c)
+ .
+
+ (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
+ Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
+ match sl with
+ | T_Leaf None => nd_id0
+ | T_Leaf (Some x) => nd_id1 x
+ | T_Branch a b => nd_prod (nd_id a) (nd_id b)
+ end.
+
+ Hint Constructors Structural.
+ Lemma nd_id_structural : forall sl, Structural (nd_id sl).
+ intros.
+ induction sl; simpl; auto.
+ destruct a; auto.
+ Defined.
+
+ (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
+ * structural variations *)
+ Class ND_Relation :=
+ { ndr_eqv : forall {h c }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _ pf1 pf2)
+ ; ndr_eqv_equivalence : forall h c, Equivalence (@ndr_eqv h c)
+
+ (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
+ ; ndr_comp_respects : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c), f === f' -> g === g' -> f;;g === f';;g'
+ ; ndr_comp_associativity : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d), (f;;g);;h === f;;(g;;h)
+ ; ndr_comp_left_identity : forall `(f:a/⋯⋯/c), nd_id _ ;; f === f
+ ; ndr_comp_right_identity : forall `(f:a/⋯⋯/c), f ;; nd_id _ === f
+
+ (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
+ ; ndr_prod_respects : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d), f===f' -> g===g' -> f**g === f'**g'
+ ; ndr_prod_associativity : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'), (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
+ ; ndr_prod_left_identity : forall `(f:a/⋯⋯/b), (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
+ ; ndr_prod_right_identity : forall `(f:a/⋯⋯/b), (f ** nd_id0) === nd_cancelr ;; f ;; nd_rlecnac
+
+ (* products and composition must distribute over each other *)
+ ; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
+
+ (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
+ ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
+ }.
+
+ (*
+ * Single-conclusion proofs; this is an alternate representation
+ * where each inference has only a single conclusion. These have
+ * worse compositionality properties than ND's, but are easier to
+ * emit as LaTeX code.
+ *)
+ Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
+ | scnd_axiom : forall c , SCND [] [c]
+ | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
+ | scnd_weak : forall c , SCND c []
+ | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
+ | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
+ .
+ Hint Constructors SCND.
+
+ Definition mkSCNDAxioms (h:Tree ??Judgment) : SCND [] h.
+ induction h.
+ destruct a.
+ apply scnd_leaf. apply scnd_axiom.
+ apply scnd_weak.
+ apply scnd_branch; auto.
+ Defined.
+
+ (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *)
+ Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
+ : forall h x c, ND x c -> SCND h x -> SCND h c.
+ intros h x c nd.
+ induction nd; intro k.
+ apply k.
+ apply k.
+ apply scnd_weak.
+ eapply scnd_branch; apply k.
+ inversion k; subst.
+ apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
+ apply IHnd2.
+ apply IHnd1.
+ apply k.
+ inversion k; subst; auto.
+ inversion k; subst; auto.
+ apply scnd_branch; auto.
+ apply scnd_branch; auto.
+ inversion k; subst; inversion X; subst; auto.
+ inversion k; subst; inversion X0; subst; auto.
+ destruct c.
+ destruct o.
+ apply scnd_leaf. eapply scnd_comp. apply k. apply r.
+ apply scnd_weak.
+ set (all_rules_one_conclusion _ _ _ r) as bogus.
+ inversion bogus.
+ Defined.
+
+ (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *)
+ Inductive ClosedND : Tree ??Judgment -> Type :=
+ | cnd_weak : ClosedND []
+ | cnd_rule : forall h c , ClosedND h -> Rule h c -> ClosedND c
+ | cnd_branch : forall c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2)
+ .
+
+ (*
+ (* we can turn an SCND without hypotheses into a ClosedND *)
+ Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
+ refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
+ (match pn2 in SCND H C return H=h -> C=c -> _ with
+ | scnd_weak c => let case_weak := tt in _
+ | scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _
+ | scnd_axiom c => let case_axiom := tt in _
+ | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
+ | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
+ let q1 := closedFromPnodes _ _ pn' in
+ let q2 := closedFromPnodes _ _ pn'' in _
+
+ end (refl_equal _) (refl_equal _))) h c pn2 cnd).
+
+ destruct case_axiom.
+ intros; subst.
+ (* FIXME *)
+
+ destruct case_comp.
+ intros.
+ clear pn2.
+ apply (cnd_rule ct).
+ apply qq.
+ subst.
+ apply cnd0.
+ apply rule.
+
+ destruct case_weak.
+ intros; subst.
+ apply cnd_weak.
+
+ destruct case_leaf.
+ intros.
+ apply qq.
+ subst.
+ apply cnd0.
+
+ destruct case_branch.
+ intros.
+ apply cnd_branch.
+ apply q1. subst. apply cnd0.
+ apply q2. subst. apply cnd0.
+ Defined.
+ *)
+
+ Close Scope nd_scope.
+ Open Scope pf_scope.
+
+End Natural_Deduction.
+
+Implicit Arguments ND [ Judgment ].
+Hint Constructors Structural.
+Hint Extern 1 => apply nd_id_structural.
+Hint Extern 1 => apply ndr_structural_indistinguishable.
+
+(* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
+ * of proofs. When only one kind of proof is in use, it's quite helpful though. *)
+Notation "H /⋯⋯/ C" := (@ND _ _ H C) : pf_scope.
+Notation "a ;; b" := (nd_comp a b) : nd_scope.
+Notation "a ** b" := (nd_prod a b) : nd_scope.
+Notation "[# a #]" := (nd_rule a) : nd_scope.
+Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope.
+
+(* enable setoid rewriting *)
+Open Scope nd_scope.
+Open Scope pf_scope.
+
+Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c))
+ symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c))
+ transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
+ as parametric_relation_ndr_eqv.
+ Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
+ with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
+ as parametric_morphism_nd_comp.
+ intros; apply ndr_comp_respects; auto.
+ Defined.
+ Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
+ with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
+ as parametric_morphism_nd_prod.
+ intros; apply ndr_prod_respects; auto.
+ Defined.
+
+(* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
+Definition nd_replicate
+ : forall
+ {Judgment}{Rule}{Ob}
+ (h:Ob->Judgment)
+ (c:Ob->Judgment)
+ (j:Tree ??Ob),
+ (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
+ @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
+ intros.
+ induction j; simpl.
+ destruct a; simpl.
+ apply X.
+ apply nd_id0.
+ apply nd_prod; auto.
+ Defined.
+
+(* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
+Definition nd_map
+ : forall
+ {Judgment}{Rule0}{Rule1}
+ (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
+ {h}{c}
+ (pf:@ND Judgment Rule0 h c)
+ ,
+ @ND Judgment Rule1 h c.
+ intros Judgment Rule0 Rule1 r.
+
+ refine ((fix nd_map h c pf {struct pf} :=
+ ((match pf
+ in @ND _ _ H C
+ return
+ @ND Judgment Rule1 H C
+ with
+ | nd_id0 => let case_nd_id0 := tt in _
+ | nd_id1 h => let case_nd_id1 := tt in _
+ | nd_weak h => let case_nd_weak := tt in _
+ | nd_copy h => let case_nd_copy := tt in _
+ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
+ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
+ | nd_rule _ _ rule => let case_nd_rule := tt in _
+ | nd_cancell _ => let case_nd_cancell := tt in _
+ | nd_cancelr _ => let case_nd_cancelr := tt in _
+ | nd_llecnac _ => let case_nd_llecnac := tt in _
+ | nd_rlecnac _ => let case_nd_rlecnac := tt in _
+ | nd_assoc _ _ _ => let case_nd_assoc := tt in _
+ | nd_cossa _ _ _ => let case_nd_cossa := tt in _
+ end))) ); simpl in *.
+
+ destruct case_nd_id0. apply nd_id0.
+ destruct case_nd_id1. apply nd_id1.
+ destruct case_nd_weak. apply nd_weak.
+ destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
+ destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
+ destruct case_nd_cancell. apply nd_cancell.
+ destruct case_nd_cancelr. apply nd_cancelr.
+ destruct case_nd_llecnac. apply nd_llecnac.
+ destruct case_nd_rlecnac. apply nd_rlecnac.
+ destruct case_nd_assoc. apply nd_assoc.
+ destruct case_nd_cossa. apply nd_cossa.
+ apply r. apply rule.
+ Defined.
+
+(* "map" over natural deduction proofs, where the result proof has different judgments *)
+Definition nd_map'
+ : forall
+ {Judgment0}{Rule0}{Judgment1}{Rule1}
+ (f:Judgment0->Judgment1)
+ (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
+ {h}{c}
+ (pf:@ND Judgment0 Rule0 h c)
+ ,
+ @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
+ intros Judgment0 Rule0 Judgment1 Rule1 f r.
+
+ refine ((fix nd_map' h c pf {struct pf} :=
+ ((match pf
+ in @ND _ _ H C
+ return
+ @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
+ with
+ | nd_id0 => let case_nd_id0 := tt in _
+ | nd_id1 h => let case_nd_id1 := tt in _
+ | nd_weak h => let case_nd_weak := tt in _
+ | nd_copy h => let case_nd_copy := tt in _
+ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
+ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
+ | nd_rule _ _ rule => let case_nd_rule := tt in _
+ | nd_cancell _ => let case_nd_cancell := tt in _
+ | nd_cancelr _ => let case_nd_cancelr := tt in _
+ | nd_llecnac _ => let case_nd_llecnac := tt in _
+ | nd_rlecnac _ => let case_nd_rlecnac := tt in _
+ | nd_assoc _ _ _ => let case_nd_assoc := tt in _
+ | nd_cossa _ _ _ => let case_nd_cossa := tt in _
+ end))) ); simpl in *.
+
+ destruct case_nd_id0. apply nd_id0.
+ destruct case_nd_id1. apply nd_id1.
+ destruct case_nd_weak. apply nd_weak.
+ destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
+ destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
+ destruct case_nd_cancell. apply nd_cancell.
+ destruct case_nd_cancelr. apply nd_cancelr.
+ destruct case_nd_llecnac. apply nd_llecnac.
+ destruct case_nd_rlecnac. apply nd_rlecnac.
+ destruct case_nd_assoc. apply nd_assoc.
+ destruct case_nd_cossa. apply nd_cossa.
+ apply r. apply rule.
+ Defined.
+
+(* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
+Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
+ | nd_property_structural : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
+ | nd_property_prod : forall h0 c0 pf0 h1 c1 pf1,
+ @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
+ | nd_property_comp : forall h0 c0 pf0 c1 pf1,
+ @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
+ | nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
+ Hint Constructors nd_property.
+
+Close Scope pf_scope.
+Close Scope nd_scope.
--- /dev/null
+(*********************************************************************************************************************************)
+(* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+Require Import NaturalDeduction.
+
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol => "'\n':[]".
+
+Section ToLatex.
+
+ Context {Judgment : Type}.
+ Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
+
+ (* the "user" must supply functions for latexifying judgments and rules *)
+ Context (judgment2latex : Judgment -> string).
+ Context (rule2latex : forall h c, Rule h c -> string).
+
+ Open Scope string_scope.
+ Notation "a +++ b" := (append a b) (at level 100).
+ Section TreeToLatex.
+ Context (emptyleaf:string).
+ Context {T:Type}.
+ Context (leaf:T -> string).
+ Fixpoint tree2latex' (j:Tree ??T) : string :=
+ match j with
+ | T_Leaf None => emptyleaf
+ | T_Leaf (Some j') => leaf j'
+ | T_Branch b1 b2 => "\left["+++tree2latex' b1+++
+ "\text{\tt{,}}"+++
+ tree2latex' b2+++"\right]"
+ end.
+ Definition tree2latex (j:Tree ??T) : string :=
+ match j with
+ | T_Leaf None => emptyleaf
+ | T_Leaf (Some j') => leaf j'
+ | T_Branch b1 b2 => tree2latex' b1+++
+ "\text{\tt{,}}"+++
+ tree2latex' b2
+ end.
+ Fixpoint list2latex (sep:string)(l:list T) : string :=
+ match l with
+ | nil => emptyleaf
+ | (a::nil) => leaf a
+ | (a::b) => (leaf a)+++sep+++(list2latex sep b)
+ end.
+ End TreeToLatex.
+
+ Definition judgments2latex (j:Tree ??Judgment) :=
+ list2latex " " judgment2latex " \\ " (leaves j).
+
+ (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
+ Section SCND_toLatex.
+ Context (hideRule : forall h c (r:Rule h c), bool).
+
+ Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
+ match pns with
+ | scnd_leaf ht c pn => SCND_toLatex pn
+ | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2
+ | scnd_weak c => ""
+ | scnd_axiom c => judgment2latex c +++ eol
+ | scnd_comp ht ct c pns rule => if hideRule _ _ rule
+ then SCND_toLatex pns
+ else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
+ SCND_toLatex pns +++ "}{" +++ eol +++
+ judgment2latex c +++ "}" +++ eol
+ end.
+ End SCND_toLatex.
+
+ (* FIXME: this doesn't actually work properly (but SCND_toLatex does!) *)
+ Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
+ match nd with
+ | nd_id0 => indent +++ "% nd_id0 " +++ eol
+ | nd_id1 h' => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol
+ | nd_weak h' => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol
+ | nd_copy h' => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
+ "}{"+++judgments2latex c+++"}" +++ eol
+ | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++
+ indent +++ "\begin{array}{c c}" +++ eol +++
+ (nd_toLatex pf1 (" "+++indent)) +++
+ indent +++ " & " +++ eol +++
+ (nd_toLatex pf2 (" "+++indent)) +++
+ indent +++ "\end{array}"
+ | nd_comp h m c pf1 pf2 => indent +++ "% comp " +++ eol +++
+ indent +++ "\begin{array}{c}" +++ eol +++
+ (nd_toLatex pf1 (" "+++indent)) +++
+ indent +++ " \\ " +++ eol +++
+ (nd_toLatex pf2 (" "+++indent)) +++
+ indent +++ "\end{array}"
+ | nd_cancell a => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol
+ | nd_cancelr a => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol
+ | nd_llecnac a => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol
+ | nd_rlecnac a => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol
+ | nd_assoc a b c => ""
+ | nd_cossa a b c => ""
+ | nd_rule h c r => rule2latex h c r
+ end.
+
+End ToLatex.
--- /dev/null
+(*********************************************************************************************************************************)
+(* Preamble: miscellaneous notations *)
+(*********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Require Import Coq.Strings.String.
+Export Coq.Unicode.Utf8.
+Export Coq.Classes.RelationClasses.
+Export Coq.Classes.Morphisms.
+Export Coq.Setoids.Setoid.
+
+Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *)
+Generalizable All Variables.
+
+Reserved Notation "a -~- b" (at level 10).
+Reserved Notation "a ** b" (at level 10).
+Reserved Notation "?? x" (at level 1).
+Reserved Notation "a ,, b" (at level 50).
+Reserved Notation "!! f" (at level 3).
+Reserved Notation "!` x" (at level 2).
+Reserved Notation "`! x" (at level 2).
+Reserved Notation "a ~=> b" (at level 70, right associativity).
+Reserved Notation "H ===> C" (at level 100).
+Reserved Notation "f >>=>> g" (at level 45).
+Reserved Notation "a ~~{ C }~~> b" (at level 100).
+Reserved Notation "f <--> g" (at level 20).
+Reserved Notation "! f" (at level 2).
+Reserved Notation "? f" (at level 2).
+Reserved Notation "# f" (at level 2).
+Reserved Notation "f '⁻¹'" (at level 1).
+Reserved Notation "a ≅ b" (at level 70, right associativity).
+Reserved Notation "C 'ᵒᴾ'" (at level 1).
+Reserved Notation "F \ a" (at level 20).
+Reserved Notation "f >>> g" (at level 45).
+Reserved Notation "a ~~ b" (at level 54).
+Reserved Notation "a ~> b" (at level 70, right associativity).
+Reserved Notation "a ≃ b" (at level 70, right associativity).
+Reserved Notation "a ≃≃ b" (at level 70, right associativity).
+Reserved Notation "a ~~> b" (at level 70, right associativity).
+Reserved Notation "F ~~~> G" (at level 70, right associativity).
+Reserved Notation "F <~~~> G" (at level 70, right associativity).
+Reserved Notation "a ⊗ b" (at level 40).
+Reserved Notation "a ⊗⊗ b" (at level 40).
+Reserved Notation "a ⊕ b" (at level 40).
+Reserved Notation "a ⊕⊕ b" (at level 40).
+Reserved Notation "f ⋉ A" (at level 40).
+Reserved Notation "A ⋊ f" (at level 40).
+Reserved Notation "- ⋉ A" (at level 40).
+Reserved Notation "A ⋊ -" (at level 40).
+Reserved Notation "a *** b" (at level 40).
+Reserved Notation "a ;; b" (at level 45).
+Reserved Notation "[# f #]" (at level 2).
+Reserved Notation "a ---> b" (at level 11, right associativity).
+Reserved Notation "a <- b" (at level 100, only parsing).
+Reserved Notation "G |= S" (at level 75).
+Reserved Notation "F -| G" (at level 75).
+Reserved Notation "a :: b" (at level 60, right associativity).
+Reserved Notation "a ++ b" (at level 60, right associativity).
+Reserved Notation "<[ t @]>" (at level 30).
+Reserved Notation "<[ t @ n ]>" (at level 30).
+Reserved Notation "<[ e ]>" (at level 30).
+Reserved Notation "'Λ' x : t :-> e" (at level 9, right associativity, x ident).
+Reserved Notation "R ==> R' " (at level 55, right associativity).
+Reserved Notation "f ○ g" (at level 100).
+Reserved Notation "a ==[ n ]==> b" (at level 20).
+Reserved Notation "a ==[ h | c ]==> b" (at level 20).
+Reserved Notation "H /⋯⋯/ C" (at level 70).
+Reserved Notation "pf1 === pf2" (at level 80).
+Reserved Notation "a |== b @@ c" (at level 100).
+Reserved Notation "f >>>> g" (at level 45).
+Reserved Notation "a >>[ n ]<< b" (at level 100).
+Reserved Notation "f **** g" (at level 40).
+Reserved Notation "C × D" (at level 40).
+Reserved Notation "C ×× D" (at level 45).
+Reserved Notation "C ⁽ºᑭ⁾" (at level 1).
+
+Reserved Notation "'<[' a '|-' t ']>'" (at level 35).
+
+Reserved Notation "Γ '∌' x" (at level 10).
+Reserved Notation "Γ '∌∌' x" (at level 10).
+Reserved Notation "Γ '∋∋' x : a ∼ b" (at level 10, x at level 99).
+Reserved Notation "Γ '∋' x : c" (at level 10, x at level 99).
+
+Reserved Notation "a ⇛ b" (at level 40).
+Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity).
+Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80).
+Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99).
+Reserved Notation "Γ '+' x : c" (at level 50, x at level 99).
+Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99).
+Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity).
+
+Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
+ (at level 52, past at level 99, present at level 50, succedent at level 50).
+
+Reserved Notation "'η'".
+Reserved Notation "'ε'".
+Reserved Notation "'★'".
+
+Notation "a +++ b" := (append a b) (at level 100).
+Close Scope nat_scope. (* so I can redefine '1' *)
+
+Delimit Scope arrow_scope with arrow.
+Delimit Scope biarrow_scope with biarrow.
+Delimit Scope garrow_scope with garrow.
+
+Notation "f ○ g" := (fun x => f(g(x))).
+Notation "?? T" := (option T).
+
+(* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
+Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
+Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
+Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
+ (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100).
+Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
+ (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100).
+
+Notation "∀ x y z u q , P" := (forall x y z u q , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
+ : type_scope.
+Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
+ (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,
+ right associativity)
+ : type_scope.
projects / coq-hetmet.git / commitdiff