Generic Classes with Unions and Intersections (Class.v)

This file contains an example of how to use the framework to formalize a type system for the purposes of Section 3. We'll specifically call out the definitions that implement things required by the framework. The type system we specify here is a simplified model for the programming language Ceylon as discussed in the paper. That is, its types Generic consist of single-argument generic types without constraints, unions, intersections, a Top type, and a Bottom type. The system is parameterized over the relations Inh and pInh. pInh is the actual inheritance relation in that it specifies the immediate inheritance declarations of classes. That is, a class declaration like
class ListOfLists<•> extends List<List<•>>
would relate ListOfLists, List, and the generic type List<•> in pInh (the • is the single type argument variable, cparameter). Inh on the other hand tracks dependencies in inheritance declarations to reason about well-foundedness (the constraints on it are specified further down). This system of inheritance essentially models just the Materials part of Material-Shape Separation to keep subtyping easy for this example, yet decidable. The only part of this that is directly required by the framework is the type specification Generic, see below.
Require Import Common.
Require Import Decide.
Require Import Tradition.
Require Import Convert.
Require Import Coq.Lists.List.
Require Import Coq.Logic.Eqdep_dec.
Require Import Max.
Require Import Wf_nat.
Require Import Lexicographic_Product.
Require Import Plus.

Module Generics.

Parameter Class : Type.
Parameter class_deq : forall c c' : Class, { c = c' } + { c = c' -> False }.

Inductive Generic
:= parameter : Generic
 | top : Generic
 | intersection : Generic -> Generic -> Generic
 | bottom : Generic
 | union : Generic -> Generic -> Generic
 | class : Class -> Generic -> Generic -> Generic.

Lemma deq (t t' : Generic) : {t = t'} + {t = t' -> False}.
revert t'. induction t; intro t'; destruct t'; try (left; reflexivity; fail); try (right; intro e; inversion e; fail).
 destruct (IHt1 t'1); destruct (IHt2 t'2); try (right; intro ei; inversion ei; auto; fail). left. subst. reflexivity.
 destruct (IHt1 t'1); destruct (IHt2 t'2); try (right; intro ei; inversion ei; auto; fail). left. subst. reflexivity.
 destruct (class_deq c c0); destruct (IHt1 t'1); destruct (IHt2 t'2); try (right; intro ei; inversion ei; auto; fail). left. subst. reflexivity.
Qed.

Module Deq <: DecidableType.
Definition U := Generic.
Definition eq_dec := deq.
End Deq.
Module UIP := DecidableEqDep Deq.
Import UIP.
Arguments UIP [x y].
Arguments UIP_refl [x].

Fixpoint fill (i o t : Generic) : Generic
:= match t with
   | parameter => o
   | top => top
   | intersection l r => intersection (fill i o l) (fill i o r)
   | bottom => bottom
   | union l r => union (fill i o l) (fill i o r)
   | class c i' o' => class c (fill o i i') (fill i o o')
   end.

Parameter Inh : Class -> Class -> Prop.
Parameter pInh : Class -> Class -> Generic -> Prop.

The Type Instantiation

This is the first part of where we fill in one part of our framework, defining Generic to be the type of types that the framework is reasoning about

Module T <: Typ.
Definition T := Generic.
End T.
Export T.

PreInh is the reflexive, transitive closure of pInh, with appropriate subsitutions for generic type arguments. It is not required by the framework per se.

Inductive PreInh (c : Class) : Class -> T -> Prop
:= rinh : PreInh c c parameter
 | tinh (c' c'' : Class) (c't c''t : T) : pInh c c' c't -> PreInh c' c'' c''t -> PreInh c c'' (fill c't c't c''t).

Decidable/Reductive Subtyping Rules

This part is required by the framework. The inductive DCon specifies the set of subtyping rules like in Sections 3.1 and 3.2 in the paper, i.e. their constructors and components. The two argument types to DCon are the types in the conclusion, i.e. a DCon t1 t2 is a rule about when t1 is a subtype of t2. Each rule has some number of premises, but that number may vary from rule to rule. For any given rule, DReq gives us a type that lets us index into that rule's premises.
  • Rules like dtop are axioms, so their premise index type is Empty.
  • Rules like dintersectionl have one premise, so their premise index type is unit.
  • Rules like dintersection or dclass have two premises, so they have two-valued premise index types. We chose different ones for different kinds of rules, but that was not actually necessary.
Finally, DAss takes a rule and a value of its premise index type and returns the corresponding premise in the form of a function that takes a position (left or right) and returns the type in that position in that premise. The rules formalized here correspond to the reductive Ceylon subtyping rules in Figure 9 in the paper (with PreInh being ≤:: and pInh being <::) combined with the reductive subtyping rules for unions and intersections in Figure 2.
NOTE: Coq doesn't like inductives being used to instantiate things required by module types, so here and in the rest of the proof, we need to define the inductive separately and then just use a (possibly local) definition to actually instantiate the required thing. The module type Rules requires components Con, Req, and Ass, which are instantiated by local definitions here after every inductive definition.

Module DRule <: Rules T.

Inductive DCon : T -> T -> Type
:= dparameter : DCon parameter parameter
 | dtop (t : T) : DCon t top
 | dintersectionl (l r t' : T) : DCon (intersection l r) t'
 | dintersectionr (l r t' : T) : DCon (intersection l r) t'
 | dintersection (t l r : T) : DCon t (intersection l r)
 | dbottom (t' : T) : DCon bottom t'
 | dunionl (t l r : T) : DCon t (union l r)
 | dunionr (t l r : T) : DCon t (union l r)
 | dunion (l r t' : T) : DCon (union l r) t'
 | dclass (c : Class) (i o : T) (c' : Class) (i' o' c't : T) : PreInh c c' c't -> DCon (class c i o) (class c' i' o').
Local Definition Con := DCon.

Definition DReq {t t' : T} (con : DCon t t') : Type
:= match con in DCon t t' return Type with
   | dparameter => Empty
   | dtop _ => Empty
   | dintersectionl _ _ _ => unit
   | dintersectionr _ _ _ => unit
   | dintersection _ _ _ => Position
   | dbottom _ => Empty
   | dunionl _ _ _ => unit
   | dunionr _ _ _ => unit
   | dunion _ _ _ => Position
   | dclass _ _ _ _ _ _ _ _ => Variance
   end.
Local Definition Req := @DReq.

Definition DAss {t t' : T} {con : DCon t t'}
:= match con as con in DCon t t' return DReq con -> Position -> T with
   | dparameter => fun req => match req with end
   | dtop _ => fun req => match req with end
   | dintersectionl l _ t' => fun _ pos => match pos with left => l | right => t' end
   | dintersectionr _ r t' => fun _ pos => match pos with left => r | right => t' end
   | dintersection t l r => fun req pos => match req, pos with _, left => t | left, right => l | right, right => r end
   | dbottom _ => fun req => match req with end
   | dunionl t l _ => fun _ pos => match pos with left => t | right => l end
   | dunionr t _ r => fun _ pos => match pos with left => t | right => r end
   | dunion l r t' => fun req pos => match req, pos with _, right => t' | left, left => l | right, left => r end
   | dclass c i o c' i' o' c't _ => fun req pos => match req, pos with
                                                   | covariant, left => fill i o c't
                                                   | covariant, right => o'
                                                   | contravariant, left => i'
                                                   | contravariant, right => fill o i c't
                                                   end
   end.
Local Definition Ass := @DAss.

End DRule.
Import DRule.

Variances for Premises

In the paper, we introduced premises as having variances already. In the formalization, this is more step-by-step, so Var is a separate function that, like Ass, takes a rule and a value of its premise index type, and returns the variance of the corresponding premise. This is required by the framework.

Module ORule <: OrientedRules T DRule.

Definition Var {t t' : T} {con : DCon t t'} : DReq con -> Variance
:= match con as con in DCon t t' return DReq con -> Variance with
   | dparameter => fun _ => covariant
   | dtop _ => fun _ => covariant
   | dintersectionl l _ t' => fun _ => covariant
   | dintersectionr _ r t' => fun _ => covariant
   | dintersection t l r => fun _ => covariant
   | dbottom _ => fun _ => covariant
   | dunionl t l _ => fun _ => covariant
   | dunionr t _ r => fun _ => covariant
   | dunion l r t' => fun _ => covariant
   | dclass c i o c' i' o' c't _ => fun req => req
   end.

End ORule.

Parameter pinh_finite : forall c : Class, { l : list (prod Class T) | forall (c' : Class) (c't : T), pInh c c' c't -> In (pair c' c't) l & forall (c' : Class) (c't : T), In (pair c' c't) l -> pInh c c' c't}.

Section WF.

Inductive Mentioned (c : Class) : T -> Prop
:= mintersectionl (l r : T) : Mentioned c l -> Mentioned c (intersection l r)
 | mintersectionr (l r : T) : Mentioned c r -> Mentioned c (intersection l r)
 | munionl (l r : T) : Mentioned c l -> Mentioned c (union l r)
 | munionr (l r : T) : Mentioned c r -> Mentioned c (union l r)
 | mclassc (i o : T) : Mentioned c (class c i o)
 | mclassi (c' : Class) (i o : T) : Mentioned c i -> Mentioned c (class c' i o)
 | mclasso (c' : Class) (i o : T) : Mentioned c o -> Mentioned c (class c' i o).

Parameter inh_wf : well_founded Inh.
Parameter pinh_inh : forall {c c' : Class} {c't : T}, pInh c c' c't -> Inh c' c.
Parameter pinh_wf : forall (c c' : Class) (c't : T), pInh c c' c't -> forall c'' : Class, Mentioned c'' c't -> Inh c'' c.

Definition Inherited (I : T -> Type) (J : Class -> Type) (c' : prod Class T) : Type
:= prod (J (fst c')) (I parameter -> I (snd c')).

Record Invariant {I : T -> Type} {J : Class -> Type} : Type := invariant {
 itop : I top;
 iintersection : forall {l r : T}, I l -> I r -> I (intersection l r);
 ibottom : I bottom;
 iunion : forall {l r : T}, I l -> I r -> I (union l r);
 iclass : forall {c : Class} {i o : T}, J c -> I i -> I o -> I (class c i o);
 iinh : forall (c : Class), (let (linh, _, _) := pinh_finite c in Prod (Inherited I J) linh) -> J c
}.
Arguments Invariant : clear implicits.

Definition pinvariant (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) : forall t : T, (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t
:= fix pinvariant (t : T) : (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t
:= match t as t return (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t with
   | parameter => fun _ ip => ip
   | top => fun _ _ => itop inv
   | intersection l r => fun mc ip => iintersection inv (pinvariant l (fun c m => mc c (mintersectionl c l r m)) ip) (pinvariant r (fun c m => mc c (mintersectionr c l r m)) ip)
   | bottom => fun _ _ => ibottom inv
   | union l r => fun mc ip => iunion inv (pinvariant l (fun c m => mc c (munionl c l r m)) ip) (pinvariant r (fun c m => mc c (munionr c l r m)) ip)
   | class c i o => fun mc' ip => let mc := mc' c (mclassc c i o)
                               in let mi := pinvariant i (fun c' m => mc' c' (mclassi c' c i o m)) ip
                               in let mo := pinvariant o (fun c' m => mc' c' (mclasso c' c i o m)) ip
                               in iclass inv mc mi mo
   end.

Definition in_prod {A : Type} {B : A -> Type} : forall l : list A, (forall a : A, In a l -> B a) -> Prod B l
:= fix in_prod (l : list A) : (forall a : A, In a l -> B a) -> Prod B l
:= match l as l return (forall a : A, In a l -> B a) -> Prod B l with
   | nil => fun _ => prod_nil _
   | cons a l => fun f => prod_cons _ a l (f a (or_introl eq_refl)) (in_prod l (fun a i => f a (or_intror i)))
   end.

Definition in_prod_eq {A : Type} {B : A -> Type} (l : list A) (f f' : forall a : A, In a l -> B a) : (forall (a : A) (inl : In a l), f a inl = f' a inl) -> in_prod l f = in_prod l f'.
induction l; simpl in *; intro ef; try reflexivity. f_equal.
 apply ef.
 apply IHl. intros a' inl. apply ef.
Qed.

Definition iinvariant (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) : forall c : Class, Acc Inh c -> J c
:= fix iinvariant (c : Class) (acc : Acc Inh c) : J c
:= match acc with
   | Acc_intro _ rec => iinh inv c match pinh_finite c as fin return let (linh, _, _) := fin in Prod (Inherited I J) linh with
                                   | exist2 _ _ linh _ fin => in_prod linh (fun (c' : prod Class T) => match c' as c' return In c' linh -> Inherited I J c' with
                                                                                                       | pair c' c't => fun i => pair (iinvariant c' (rec c' (pinh_inh (fin c' c't i)))) (pinvariant _ _ inv c't (fun c'' m => iinvariant c'' (rec c'' (pinh_wf c c' c't (fin c' c't i) c'' m))))
                                                                                                       end)
                                   end
   end.

Definition cinvariant {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (c : Class) : J c
:= iinvariant I J inv c (inh_wf c).
Definition tinvariant {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (t : T) : I parameter -> I t
:= pinvariant I J inv t (fun c _ => cinvariant inv c).

Lemma tinvariant_eq {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (t : T) (ip : I parameter)
: tinvariant inv t ip
= match t with
  | parameter => ip
  | top => itop inv
  | intersection l r => iintersection inv (tinvariant inv l ip) (tinvariant inv r ip)
  | bottom => ibottom inv
  | union l r => iunion inv (tinvariant inv l ip) (tinvariant inv r ip)
  | class c i o => iclass inv (cinvariant inv c) (tinvariant inv i ip) (tinvariant inv o ip)
  end.
destruct t; auto.
Qed.

Definition pinvariant_eq (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) (t : T) (mc mc' : forall c : Class, Mentioned c t -> J c) : (forall (c : Class) (m : Mentioned c t), mc c m = mc' c m) -> pinvariant I J inv t mc = pinvariant I J inv t mc'.
revert mc mc'. induction t; simpl; intros mc mc' ec; try reflexivity.
 erewrite IHt1. erewrite IHt2. reflexivity.
  simpl. intros c m. apply ec.
  simpl. intros c m. apply ec.
 erewrite IHt1. erewrite IHt2. reflexivity.
  simpl. intros c m. apply ec.
  simpl. intros c m. apply ec.
 erewrite IHt1. erewrite IHt2. rewrite ec. reflexivity.
  simpl. intros c' m. apply ec.
  simpl. intros c' m. apply ec.
Qed.

Definition map_prod {A : Type} {B : A -> Type} (f : forall a : A, B a) : forall l : list A, Prod B l
:= fix in_prod (l : list A) : Prod B l
:= match l as l return Prod B l with
   | nil => prod_nil _
   | cons a l => prod_cons _ a l (f a) (in_prod l)
   end.

Lemma iinvariant_eq (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) (c : Class) (acc acc' : Acc Inh c) : iinvariant I J inv c acc = iinvariant I J inv c acc'.
revert c acc acc'. fix 2. intros c acc acc'. destruct acc as [ acc ]. destruct acc' as [ acc' ]. simpl. f_equal. destruct (pinh_finite c) as [ linh _ fin ]. apply in_prod_eq. intros [ c' c't ] inl. f_equal.
 apply iinvariant_eq.
 apply pinvariant_eq. intros c'' m. apply iinvariant_eq.
Qed.

Lemma cinvariant_eq {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (c : Class)
: cinvariant inv c
= iinh inv c match pinh_finite c as fin return let (linh, _, _) := fin in Prod (Inherited I J) linh with
             | exist2 _ _ linh _ _ => map_prod (fun (c' : prod Class T) => match c' as c' return Inherited I J c' with
                                                                           | pair c' c't => pair (cinvariant inv c') (tinvariant inv c't)
                                                                           end) linh
             end.
unfold cinvariant. generalize (inh_wf c). revert c. fix 2. intros c acc. destruct acc as [ acc ]. simpl. f_equal. destruct (pinh_finite c) as [ linh _ fin ]. induction linh; simpl; try reflexivity. f_equal.
 destruct a as [ c' c't ]. f_equal.
  apply iinvariant_eq.
  unfold tinvariant. apply pinvariant_eq. intros c'' m. unfold cinvariant. apply iinvariant_eq.
 rewrite <- IHlinh with (fun c t inl => fin c t (or_intror inl)). apply in_prod_eq. intros [ c' c't ] inl. reflexivity.
Qed.

Definition prod_list {A : Type} {B : Type} : forall {l : list A}, Prod (fun _ => B) l -> list B
:= fix prod_list (l : list A) (p : Prod (fun _ => B) l) : list B
:= match p with
   | prod_nil _ => nil
   | prod_cons _ _ l b p => cons b (prod_list l p)
   end.

Definition Measure (M N : Type) : Type
:= Invariant (fun _ => M) (fun _ => N).
Definition measure (M N : Type)
 (mtop : M)
 (mintersection : M -> M -> M)
 (mbottom : M)
 (munion : M -> M -> M)
 (mclass : N -> M -> M -> M)
 (minh_init : N)
 (minh_iter : N -> N -> (M -> M) -> N)
 : Measure M N.
apply invariant.
 exact mtop.
 intros _ _. exact mintersection.
 exact mbottom.
 intros _ _. exact munion.
 intros _ _ _. exact mclass.
 intros c p. destruct (pinh_finite c) as [ linh _ _ ]. unfold Inherited in p. exact (fold_right (fun c' c => minh_iter c (fst c') (snd c')) minh_init (prod_list p)).
Defined.

Definition expansion : Measure nat (nat -> nat -> nat).
apply measure.
 exact 0.
 intros ml mr. exact (S (max ml mr)).
 exact 0.
 intros ml mr. exact (S (max ml mr)).
 intros mc mi mo. exact (S (mc mi mo)).
 exact max.
 intros mc mc' mt mi mo. exact (max (mc mi mo) (mc' (mt (max mo mi)) (mt (max mi mo)))).
Defined.

Definition texpansion := tinvariant expansion.
Definition cexpansion := cinvariant expansion.

Lemma max_mono (l l' r r' : nat) : l <= l' -> r <= r' -> max l r <= max l' r'.
intros ll lr. apply max_lub.
 etransitivity; [ exact ll | apply le_max_l ].
 etransitivity; [ exact lr | apply le_max_r ].
Qed.

Lemma expansion_mono : Invariant (fun t => forall mp mp' : nat, mp <= mp' -> texpansion t mp <= texpansion t mp') (fun c => forall mi mi' mo mo' : nat, mi <= mi' -> mo <= mo' -> cexpansion c mi mo <= cexpansion c mi' mo').
apply invariant.
 unfold texpansion. intros mp mp' lp. repeat rewrite (tinvariant_eq _ top). reflexivity.
 intros l r ll lr mp mp' lp. unfold texpansion. repeat rewrite (tinvariant_eq _ (intersection _ _)). simpl. apply le_n_S. apply max_mono; auto.
 unfold texpansion. intros mp mp' lp. repeat rewrite (tinvariant_eq _ bottom). reflexivity.
 intros l r ll lr mp mp' lp. unfold texpansion. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. apply le_n_S. apply max_mono; auto.
 intros c i o lc li lo mp mp' lp. unfold texpansion. repeat rewrite (tinvariant_eq _ (class _ _ _)). simpl. apply le_n_S. apply lc; auto.
 intros c p mi mi' mo mo'. unfold cexpansion. repeat rewrite (cinvariant_eq _ c). simpl. destruct (pinh_finite c) as [ linh _ _ ]. revert mi mi' mo mo'. induction p; simpl in *.
  intros mi mi' mo mo' li lo. apply max_mono; assumption.
  destruct a as [ c' c't ]. intros mi mi' mo mo' li lo. apply max_mono.
   apply IHp; assumption.
   simpl. unfold Inherited in b. destruct b as [ lc' lt ]. apply lc'; apply lt.
    intros mp mp' lp. unfold texpansion. repeat rewrite (tinvariant_eq _ parameter). assumption.
    apply max_mono; assumption.
    intros mp mp' lp. unfold texpansion. repeat rewrite (tinvariant_eq _ parameter). assumption.
    apply max_mono; assumption.
Qed.

Lemma texpansion_mono (mp mp' : nat) (t : T) : mp <= mp' -> texpansion t mp <= texpansion t mp'.
revert mp mp'. apply (tinvariant expansion_mono). clear t. unfold texpansion. intros mp mp' lp. repeat rewrite (tinvariant_eq _ parameter). assumption.
Qed.

Lemma cexpansion_mono (c : Class) (mi mi' mo mo' : nat) : mi <= mi' -> mo <= mo' -> cexpansion c mi mo <= cexpansion c mi' mo'.
revert c mi mi' mo mo'. apply (cinvariant expansion_mono).
Qed.

Lemma cexpansion_i (c : Class) (mi mo : nat) : mi <= cexpansion c mi mo.
unfold cexpansion. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh _ _ ]. induction linh; simpl.
 apply le_max_l.
 destruct a as [ c' c't ]. etransitivity; [ apply IHlinh | ]. apply le_max_l.
Qed.

Lemma cexpansion_o (c : Class) (mi mo : nat) : mo <= cexpansion c mi mo.
unfold cexpansion. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh _ _ ]. induction linh; simpl.
 apply le_max_r.
 destruct a as [ c' c't ]. etransitivity; [ apply IHlinh | ]. apply le_max_l.
Qed.

Lemma cexpansion_inh (c : Class) (mi mo : nat) (c' : Class) (c't : T) (pinh : pInh c c' c't) : cexpansion c' (texpansion c't (max mo mi)) (texpansion c't (max mi mo)) <= cexpansion c mi mo.
unfold cexpansion. rewrite (cinvariant_eq _ c). simpl. destruct (pinh_finite c) as [ linh fin _ ]. apply fin in pinh. clear fin. induction linh; simpl in *.
 destruct pinh.
 destruct pinh as [ e | inl ].
  subst. apply le_max_r.
  etransitivity; [ | apply le_max_l ]. apply IHlinh; assumption.
Qed.

Lemma fexpansion (i o t : T) (mp : nat) : texpansion (fill i o t) mp <= texpansion t (max (texpansion i mp) (texpansion o mp)).
revert i o mp. induction t; intros i o mp; simpl.
 unfold texpansion. rewrite (tinvariant_eq _ parameter). apply le_max_r.
 unfold texpansion. repeat rewrite (tinvariant_eq _ top). reflexivity.
 unfold texpansion. repeat rewrite (tinvariant_eq _ (intersection _ _)). simpl. apply le_n_S. apply max_mono; auto.
 unfold texpansion. repeat rewrite (tinvariant_eq _ bottom). reflexivity.
 unfold texpansion. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. apply le_n_S. apply max_mono; auto.
 unfold texpansion. repeat rewrite (tinvariant_eq _ (class _ _ _)). simpl. apply le_n_S. apply cexpansion_mono.
  etransitivity; [ apply IHt1 | ]. apply texpansion_mono. apply max_lub; [ apply le_max_r | apply le_max_l ].
  apply IHt2.
Qed.

Lemma fill_fill (i o i' o' t : T) : fill i o (fill i' o' t) = fill (fill o i i') (fill i o o') t.
revert i o i' o'. induction t; intros i o i' o'; try (simpl; reflexivity).
 simpl. apply f_equal2; trivial.
 simpl. apply f_equal2; trivial.
 simpl. apply f_equal2; trivial.
Qed.

Lemma wf (R : T -> T -> Type) : (forall t1 t2 : T, (forall (con : DCon t1 t2) (req : DReq con), R (DAss req left) (DAss req right)) -> R t1 t2) -> forall t t' : T, R t t'.
intros rec t t'. pose proof (well_founded_ltof (prod T T) (fun tt' => let (t, t') := tt' in plus (texpansion t 0) (texpansion t' 0)) (pair t t')) as acc. change (R (fst (pair t t')) (snd (pair t t'))). revert acc. generalize (pair t t'). clear t t'. intros tt' acc. induction acc as [ tt' _ ind ]. destruct tt' as [ t t' ]. simpl in *. apply rec. clear rec. intros con req. apply (ind (pair _ _)); clear ind. unfold ltof. simpl. destruct con; try (destruct req; fail).
 unfold texpansion at 3. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold texpansion. unfold lt. apply le_n_S. apply plus_le_compat_r. apply le_max_l.
 unfold texpansion at 3. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold texpansion. unfold lt. apply le_n_S. apply plus_le_compat_r. apply le_max_r.
 unfold texpansion at 4. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold texpansion. unfold lt. rewrite <- plus_Snm_nSm. simpl. apply le_n_S. apply plus_le_compat.
  destruct req; reflexivity.
  destruct req; [ apply le_max_l | apply le_max_r ].
 unfold texpansion at 4. rewrite (tinvariant_eq _ (union l r)). simpl. fold texpansion. unfold lt. rewrite <- plus_Snm_nSm. simpl. apply le_n_S. apply plus_le_compat_l. apply le_max_l.
 unfold texpansion at 4. rewrite (tinvariant_eq _ (union l r)). simpl. fold texpansion. unfold lt. rewrite <- plus_Snm_nSm. simpl. apply le_n_S. apply plus_le_compat_l. apply le_max_r.
 unfold texpansion at 3. rewrite (tinvariant_eq _ (union l r)). simpl. fold texpansion. unfold lt. apply le_n_S. apply plus_le_compat.
  destruct req; [ apply le_max_l | apply le_max_r ].
  destruct req; reflexivity.
 unfold texpansion at 3 4. repeat rewrite (tinvariant_eq _ (class _ _ _)). simpl. fold texpansion. fold cexpansion. unfold lt. rewrite <- plus_Snm_nSm. simpl. apply le_S. apply le_n_S. destruct req.
  apply plus_le_compat.
   clear i' o'. revert i o. induction p; simpl; intros i o.
    apply cexpansion_o.
    rewrite fill_fill. etransitivity; [ apply IHp | ]. etransitivity; [ | apply cexpansion_inh; exact H ]. apply cexpansion_mono; apply fexpansion.
   apply cexpansion_o.
  rewrite plus_comm. apply plus_le_compat.
   clear i' o'. revert i o. induction p; simpl; intros i o.
    apply cexpansion_i.
    rewrite fill_fill. etransitivity; [ apply IHp | ]. etransitivity; [ | apply cexpansion_inh; exact H ]. apply cexpansion_mono; apply fexpansion.
   apply cexpansion_i.
Qed.

End WF.

Reflexivity and Transitivity

The next part in specifying decidable/reductive subtyping in our framework are the requirements that have to do with reflexivity, transitivity, and well-foundedness. In this module refl, Red, finite_con, and wf (the last of which was just defined above and will basically be imported here) are required by the framework. Their correspondences are explained in Decide.v, and their meaning is straightforward. The defintions of everything but refl are somewhat tedious, but that is to be expected of formalizing a type system with a medium amount of complexity in Coq. The point of our framework is that all of this proof-work can be reused for extensions to the type system.

Module DDRule <: DecidableRules T DRule ORule.
Module Reduction := Reduction T DRule ORule.
Import Reduction.
Module Proof := Reduction.Proof .
Import Proof.
Module ProofPV := Reduction.ProofPV.
Import ProofPV.

Lemma refl (t : T) : Proof t t.
induction t.
 apply (proof dparameter). simpl. intro req. destruct req.
 apply (proof (dtop _)). simpl. intro req. destruct req.
 apply (proof (dintersection _ _ _)). simpl. intro req. destruct req.
  apply (proof (dintersectionl _ _ _)). simpl. intros _. assumption.
  apply (proof (dintersectionr _ _ _)). simpl. intros _. assumption.
 apply (proof (dbottom _)). simpl. intro req. destruct req.
 apply (proof (dunion _ _ _)). simpl. intro req. destruct req.
  apply (proof (dunionl _ _ _)). simpl. intros _. assumption.
  apply (proof (dunionr _ _ _)). simpl. intros _. assumption.
 apply (proof (dclass _ _ _ _ _ _ parameter (rinh _))). simpl. intro req. destruct req; assumption.
Qed.

Lemma fill_parameter (t : T) : fill parameter parameter t = t.
induction t; try (simpl; reflexivity).
 simpl. rewrite IHt1. rewrite IHt2. reflexivity.
 simpl. rewrite IHt1. rewrite IHt2. reflexivity.
 simpl. rewrite IHt1. rewrite IHt2. reflexivity.
Qed.

Lemma fill_Rv (R : Variance -> T -> T -> Prop) (admits : AdmitsPV R) {v : Variance} {i o i' o' t : T} : R (invert v) i' i -> R v o o' -> R v (fill i o t) (fill i' o' t).
revert v i o i' o'. induction t; intros v i o i' o' ri ro; simpl.
 assumption.
 apply (admits _ _ _ (dtop _)). intro req. destruct req.
 apply (admits _ _ _ (dintersection _ _ _)). simpl. intro req. destruct req.
  apply (admits _ _ _ (dintersectionl _ _ _)). simpl. intros _. destruct v; apply IHt1; assumption.
  apply (admits _ _ _ (dintersectionr _ _ _)). simpl. intros _. destruct v; apply IHt2; assumption.
 apply (admits _ _ _ (dbottom _)). simpl. intro req. destruct req.
 apply (admits _ _ _ (dunion _ _ _)). simpl. intro req. destruct req.
  apply (admits _ _ _ (dunionl _ _ _)). simpl. intros _. destruct v; apply IHt1; assumption.
  apply (admits _ _ _ (dunionr _ _ _)). simpl. intros _. destruct v; apply IHt2; assumption.
 apply (admits _ _ _ (dclass _ _ _ _ _ _ parameter (rinh _))). simpl. intro req. destruct req; destruct v; (apply IHt1 || apply IHt2); assumption.
Qed.

Lemma Red {t1 t2 t3 : T} (lcon : DCon t1 t2) (rcon : DCon t2 t3) : Reduction lcon rcon.
assert (forall {t1 t2 t2' t3 : T} (lcon : DCon t1 t2) (rcon : DCon t2' t3) (e : t2 = t2'), Reduction lcon match (eq_sym e) in _ = t return DCon t t3 with eq_refl => rcon end) as Red; [ clear t1 t2 t3 lcon rcon; intros t1 t2 t2' t3 lcon rcon e | exact (Red t1 t2 t2 t3 lcon rcon eq_refl) ].
remember lcon as lcon'; destruct lcon'.
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  apply progress with dparameter. intro req. destruct req.
  destruct e. apply progress with (dintersection _ _ _). simpl. intro req. apply permitV. apply transr. apply compose with parameter.
   destruct req; apply (proofPV _ dparameter); intro req; destruct req.
   destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with parameter.
   apply (proofPV _ dparameter). intro req. destruct req.
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with parameter.
   apply (proofPV _ dparameter). intro req. destruct req.
   apply (requires (dunionr _ _ _) tt).
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  apply progress with (dintersection _ _ _). simpl. intro req. apply permitV. apply transr. apply compose with top.
   destruct req; apply (proofPV _ (dtop _)); intro req; destruct req.
   subst. destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with top.
   apply (proofPV _ (dtop _)). intro req. destruct req.
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with top.
   apply (proofPV _ (dtop _)). intro req. destruct req.
   apply (requires (dunionr _ _ _) tt).
 subst. apply progress with (dintersectionl _ _ _). simpl. intros _. apply permitV. apply transl. apply compose with t2'.
  apply (requires (dintersectionl _ _ _) tt).
  apply (proofPV _ rcon). intro req. apply permitV. apply requires.
 subst. apply progress with (dintersectionr _ _ _). simpl. intros _. apply permitV. apply transl. apply compose with t2'.
  apply (requires (dintersectionr _ _ _) tt).
  apply (proofPV _ rcon). intro req. apply permitV. apply requires.
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  inversion e. destruct H0. destruct H1. rewrite (UIP_refl e). clear e. apply simplify with tt; try trivial. simpl. apply permitV. apply (requires (dintersection _ _ _) left).
  inversion e. destruct H0. destruct H1. rewrite (UIP_refl e). clear e. apply simplify with tt; try trivial. simpl. apply permitV. apply (requires (dintersection _ _ _) right).
  apply progress with (dintersection _ _ _). intro req. apply permitV. apply transr. destruct e. simpl. apply compose with (intersection l r).
   destruct req; apply (proofPV _ (dintersection _ _ _)); intro req; destruct req; apply permitV.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
   destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (intersection l r).
   apply (proofPV _ (dintersection _ _ _)); intro req; destruct req; apply permitV.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (intersection l r).
   apply (proofPV _ (dintersection _ _ _)); intro req; destruct req; apply permitV.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
   apply (requires (dunionr _ _ _) tt).
 apply progress with (dbottom _). intro req. destruct req.
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  apply progress with (dintersection _ _ _). simpl. intro req. apply permitV. apply transr. apply compose with (union l r).
   destruct req; apply (proofPV _ (dunionl _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionl _ _ _) tt).
   subst. destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (union l r).
   apply (proofPV _ (dunionl _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionl _ _ _) tt).
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (union l r).
   apply (proofPV _ (dunionl _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionl _ _ _) tt).
   apply (requires (dunionr _ _ _) tt).
  inversion e. destruct H0. destruct H1. rewrite (UIP_refl e). clear e. apply simplify with left; try trivial. simpl. apply permitV. apply (requires (dunionl _ _ _) tt).
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  apply progress with (dintersection _ _ _). simpl. intro req. apply permitV. apply transr. apply compose with (union l r).
   destruct req; apply (proofPV _ (dunionr _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionr _ _ _) tt).
   subst. destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (union l r).
   apply (proofPV _ (dunionr _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionr _ _ _) tt).
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (union l r).
   apply (proofPV _ (dunionr _ _ _)); intro req; destruct req; apply permitV; apply (requires (dunionr _ _ _) tt).
   apply (requires (dunionr _ _ _) tt).
  inversion e. destruct H0. destruct H1. rewrite (UIP_refl e). clear e. apply simplify with right; try trivial. simpl. apply permitV. apply (requires (dunionr _ _ _) tt).
 subst. apply progress with (dunion _ _ _). simpl. intros req. destruct req; apply permitV; apply transl; apply compose with t2'.
  apply (requires (dunion _ _ _) left).
  apply (proofPV _ rcon). intro req. apply permitV. apply requires.
  apply (requires (dunion _ _ _) right).
  apply (proofPV _ rcon). intro req. apply permitV. apply requires.
 remember rcon as rcon'; destruct rcon'; try (inversion e; fail); try (apply progress with (dtop _); intro req; destruct req).
  apply progress with (dintersection _ _ _). simpl. intro req. apply permitV. apply transr. apply compose with (class c' i' o').
   destruct req; apply (proofPV _ (dclass _ _ _ _ _ _ c't p)); intro req; destruct req; apply permitV; simpl.
    apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
    apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
    apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
    apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
   subst. destruct req.
    apply (requires (dintersection _ _ _) left).
    apply (requires (dintersection _ _ _) right).
  apply progress with (dunionl _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (class c' i' o').
   apply (proofPV _ (dclass _ _ _ _ _ _ c't p)); intro req; destruct req; apply permitV; simpl.
    apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
    apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
   apply (requires (dunionl _ _ _) tt).
  apply progress with (dunionr _ _ _). simpl. intros _. apply permitV. apply transr. destruct e. apply compose with (class c' i' o').
   apply (proofPV _ (dclass _ _ _ _ _ _ c't p)); intro req; destruct req; apply permitV; simpl.
    apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
    apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
   apply (requires (dunionr _ _ _) tt).
  inversion e. destruct H0. destruct H1. destruct H2. rewrite (UIP_refl e). clear e. rename c'0 into c''. rename i'0 into i''. rename o'0 into o''. rename c't0 into c''t. rename p0 into p'. assert (PreInh c c'' (fill c't c't c''t)) as p''.
   clear lcon Heqlcon' rcon Heqrcon' i o i' o' i'' o''. revert c'' c''t p'. induction p.
    intros c'' c''t p'. rewrite fill_parameter. assumption.
    intros c''' c'''t p''. rewrite <- fill_fill. apply tinh with c'; try trivial. apply IHp. assumption.
   apply progress with (dclass c i o c'' i'' o'' _ p''). simpl. intro req. apply permitV. destruct req.
    apply transr. apply compose with (fill i' o' c''t).
     rewrite fill_fill. apply fill_Rv.
      apply proof_admitsPV.
      simpl. apply permitV. apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
      simpl. apply permitV. apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
     apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
    apply transr. apply contrapose with (fill o' i' c''t).
     apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
     rewrite fill_fill. apply fill_Rv.
      apply proof_admitsPV.
      simpl. apply permitV. apply (requires (dclass _ _ _ _ _ _ _ _) covariant).
      simpl. apply permitV. apply (requires (dclass _ _ _ _ _ _ _ _) contravariant).
Qed.

Lemma preinh_finite : forall c : Class, { l : list (prod Class T) | forall (c' : Class) (c't : T), PreInh c c' c't -> In (pair c' c't) l & forall (c' : Class) (c't : T), In (pair c' c't) l -> PreInh c c' c't}.
intro c. pose proof (inh_wf c) as acc. induction acc as [ c _ ind ]. pose proof (pinh_finite c) as finite. destruct finite as [ linh fin inh ]. assert {l : list (prod Class T) | forall (c' : Class) (c't : T), In (pair c' c't) linh -> forall (c'' : Class) (c''t : T), PreInh c' c'' c''t -> In (c'', fill c't c't c''t) l & forall (c' : Class) (c't : T), In (c', c't) l -> PreInh c c' c't } as finite.
 clear fin. induction linh.
  apply exist2 with nil; simpl; intros _ _ [].
  simpl in inh. pose proof (IHlinh (fun c' c't inl => inh c' c't (or_intror inl))) as IHlinh. destruct a as [ c' c't ]. pose proof (inh c' c't (or_introl eq_refl)) as p. pose proof (ind c' (pinh_inh p)) as ind. destruct ind as [ lind finind inhind ]. destruct IHlinh as [ lrec finrec inhrec ]. apply exist2 with (app (map (fun c'' => pair (fst c'') (fill c't c't (snd c''))) lind) lrec); simpl.
   intros c'' c''t inl c''' c'''t p'. apply in_or_app. destruct inl as [ e | inl ].
    left. inversion e. clear e. destruct H0. destruct H1. apply finind in p'. apply (fun l => in_map (fun c'' => (fst c'', fill c't c't (snd c''))) l (c''', c'''t)). assumption.
    right. apply finrec with c''; assumption.
   intros c''' c'''t inl. apply in_app_or in inl. destruct inl as [ inl | inl ].
    apply in_map_iff in inl. destruct inl as [ [ c'' c''t ] [ e inl ] ]. simpl in e. inversion e. clear e. destruct H0. destruct H1. apply tinh with c'; try assumption. apply inhind. assumption.
    apply inhrec. assumption.
 destruct finite as [ linh' fin' inh' ]. apply exist2 with (cons (pair c parameter) linh'); simpl.
  intros c'' c''t pre. destruct pre.
   left. reflexivity.
   right. eapply fin'; try exact pre. apply fin. assumption.
  intros c' c't inl. destruct inl as [ e | inl ].
   inversion e. clear e. apply rinh.
   apply inh'. assumption.
Qed.

Definition map_filter {A B : Type} (f : A -> option B) : list A -> list B
:= fix map_filter (l : list A) : list B
:= match l with
   | nil => nil
   | cons a l => match f a with
                 | None => map_filter l
                 | Some b => cons b (map_filter l)
                 end
   end.

Lemma exists_map_filter {A B : Type} (f : A -> option B) (l : list A) (a : A) (b : B) : f a = Some b -> In a l -> In b (map_filter f l).
intros e inl. induction l as [ | a' l rec ]; simpl in *.
 assumption.
 destruct inl as [ ea | inl ].
  subst. destruct (f a) as [ b' | ].
   inversion e. clear e. subst. left. reflexivity.
   inversion e.
  destruct (f a') as [ b' | ].
   right. apply rec. assumption.
   apply rec. assumption.
Qed.

Lemma map_filter_exists {A B : Type} (f : A -> option B) (l : list A) (b : B) : In b (map_filter f l) -> exists2 a : A, f a = Some b & In a l.
intro inl. induction l as [ | a' l rec ]; simpl in *.
 destruct inl.
 remember (f a') as fa. destruct fa as [ b' | ].
  destruct inl as [ e | inl ].
   subst. apply ex_intro2 with a'; auto.
   destruct rec as [ a e inl' ]; try assumption. apply ex_intro2 with a; try assumption. right. assumption.
   destruct rec as [ a e inl' ]; try assumption. apply ex_intro2 with a; try assumption. right. assumption.
Qed.

Lemma preinh_dec (c c' : Class) : { linh : list T | forall t : T, In t linh -> PreInh c c' t & forall t : T, PreInh c c' t -> In t linh }.
pose proof (preinh_finite c) as [ linh fin inh ]. apply exist2 with (map_filter (fun c'' => if class_deq c' (fst c'') then Some (snd c'') else None) linh).
 intros t inl. apply inh. apply map_filter_exists in inl. destruct inl as [ [ c'' c''t ] e inl ]. simpl in e. destruct (class_deq c' c'') as [ ec | ne ].
  destruct ec. inversion e. clear e. destruct H0. assumption.
  inversion e.
 intros t p. apply fin in p. apply exists_map_filter with (c', t); try assumption. simpl. destruct (class_deq c' c') as [ _ | ne ]; try reflexivity. destruct (ne eq_refl).
Qed.

Definition in_map {A B : Type} : forall l : list A, (forall a : A, In a l -> B) -> list B
:= fix in_map (l : list A) : (forall a : A, In a l -> B) -> list B
:= match l as l return (forall a : A, In a l -> B) -> list B with
   | nil => fun _ => nil
   | cons a l => fun f => cons (f a (or_introl eq_refl)) (in_map l (fun a i => f a (or_intror i)))
   end.

Definition FiniteCon (t t' : T) : Type := { lcon : list (DCon t t')
                                          & Prod (fun con : DCon t t' => { lreq : list (DReq con) | forall req : DReq con, In req lreq }) lcon
                                          & forall R : T -> T -> Prop, Admits R -> (forall {t1 t2 t3 t4 : T}, Proof t1 t2 -> R t2 t3 -> Proof t3 t4 -> R t1 t4) -> forall con' : DCon t t', (forall req : DReq con', R (DAss req left) (DAss req right)) -> Exists (fun con : DCon t t' => forall req : DReq con, R (DAss req left) (DAss req right)) lcon }.

Lemma finite_con {t t' : T} : FiniteCon t t'.
assert (forall t t', (forall t1 t2 : T, t1 = t -> t2 = t' -> DCon t1 t2 -> False) -> FiniteCon t t') as fnone. clear t t'. intros t t' f. apply existT2 with nil.
 apply prod_nil.
 intros R _ _ con'. destruct (f t t' eq_refl eq_refl con').
assert (forall t, FiniteCon t top) as ftop. clear t t'. intro t. apply existT2 with (cons (dtop t) nil).
 apply prod_cons; try apply prod_nil. apply exist with nil. intro req. destruct req.
 intros R admits trans con' ass'. apply Exists_cons_hd. intro req. destruct req.
assert (forall t l r, FiniteCon t (intersection l r)) as fintersection. clear t t'. intros t l r. apply existT2 with (cons (dintersection t l r) nil).
 apply prod_cons; try apply prod_nil. apply exist with (cons left (cons right nil)). intro req. destruct req; simpl; auto.
 generalize (eq_refl (intersection l r)). generalize (intersection l r) at 2 3 4 5 6. intros t' e R admits trans con' ass'. apply Exists_cons_hd. simpl. intro req. destruct con'; try (inversion e; fail); simpl in ass'.
  subst. pose proof (ass' tt) as ass'. simpl. destruct req; apply (admits _ _ (dintersectionl _ _ _)); simpl; intros _; apply (trans _ _ _ _ (refl _) ass').
   apply proof with (dintersectionl _ _ _). simpl. intros _. apply refl.
   apply proof with (dintersectionr _ _ _). simpl. intros _. apply refl.
  subst. pose proof (ass' tt) as ass'. simpl. destruct req; apply (admits _ _ (dintersectionr _ _ _)); simpl; intros _; apply (trans _ _ _ _ (refl _) ass').
   apply proof with (dintersectionl _ _ _). simpl. intros _. apply refl.
   apply proof with (dintersectionr _ _ _). simpl. intros _. apply refl.
  inversion e. clear e. subst. apply ass'.
  destruct req; apply (admits _ _ (dbottom _)); intro req'; destruct req'.
  subst. destruct req.
   apply (admits _ _ (dunion _ _ _)). simpl. intro req'. destruct req'.
    apply (trans _ _ _ _ (refl _) (ass' left)). apply proof with (dintersectionl _ _ _). simpl. intros _. apply refl.
    apply (trans _ _ _ _ (refl _) (ass' right)). apply proof with (dintersectionl _ _ _). simpl. intros _. apply refl.
   apply (admits _ _ (dunion _ _ _)). simpl. intro req'. destruct req'.
    apply (trans _ _ _ _ (refl _) (ass' left)). apply proof with (dintersectionr _ _ _). simpl. intros _. apply refl.
    apply (trans _ _ _ _ (refl _) (ass' right)). apply proof with (dintersectionr _ _ _). simpl. intros _. apply refl.
assert (forall t l r, (forall t1 t2 : T, t = t1 -> t2 = union l r -> forall con' : DCon t1 t2, match con' with dunionl _ _ _ => True | dunionr _ _ _ => True | _ => False end) -> FiniteCon t (union l r)) as funion. clear t t'. intros t l r ec. apply existT2 with (cons (dunionl t l r) (cons (dunionr t l r) nil)).
 apply prod_cons; try apply prod_cons; try apply prod_nil; apply exist with (cons tt nil); intros req; destruct req; simpl; auto.
 generalize (eq_refl (union l r)). generalize (union l r) at 2 3 4 5 6. intros t' e' R admits trans con' ass'. pose proof (ec _ _ eq_refl (eq_sym e') con') as ec. destruct con'; destruct ec.
  inversion e'. subst. apply Exists_cons_hd. assumption.
  inversion e'. subst. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
destruct t.
 destruct t'; try (apply ftop || apply fintersection || apply fnone; intros t t' e e' con; destruct con; inversion e; inversion e'; fail).
  apply existT2 with (cons dparameter nil).
   apply prod_cons; try apply prod_nil. apply exist with nil. intro req. destruct req.
   intros R admits trans con' ass'. apply Exists_cons_hd. intro req. destruct req.
  apply funion. intros t1 t2 e1 e2 con'. destruct con'; inversion e1; inversion e2; exact I.
 destruct t'; try (apply ftop || apply fintersection || apply fnone; intros t t' e e' con; destruct con; inversion e; inversion e'; fail). apply funion. intros t1 t2 e1 e2 con'. destruct con'; inversion e1; inversion e2; exact I.
 rename t1 into l. rename t2 into r. destruct t'; try (apply ftop || apply fintersection || apply fnone; intros t t' e e' con; destruct con; inversion e; inversion e'; fail).
  apply existT2 with (cons (dintersectionl l r parameter) (cons (dintersectionr l r parameter) nil)).
   apply prod_cons; try apply prod_cons; try apply prod_nil; apply exist with (cons tt nil); intros req; destruct req; simpl; auto.
   generalize (eq_refl parameter). generalize (eq_refl (intersection l r)). generalize parameter at 2 3 4 5 6. generalize (intersection l r) at 2 3 4 5 6. intros t t' e e' R admits trans con' ass'. destruct con'; try (inversion e; inversion e'; fail).
    inversion e. subst. apply Exists_cons_hd. assumption.
    inversion e. subst. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
  apply existT2 with (cons (dintersectionl l r bottom) (cons (dintersectionr l r bottom) nil)).
   apply prod_cons; try apply prod_cons; try apply prod_nil; apply exist with (cons tt nil); intros req; destruct req; simpl; auto.
   generalize (eq_refl bottom). generalize (eq_refl (intersection l r)). generalize bottom at 2 3 4 5 6. generalize (intersection l r) at 2 3 4 5 6. intros t t' e e' R admits trans con' ass'. destruct con'; try (inversion e; inversion e'; fail).
    inversion e. subst. apply Exists_cons_hd. assumption.
    inversion e. subst. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
  rename t'1 into l'. rename t'2 into r'. apply existT2 with (cons (dintersectionl l r (union l' r')) (cons (dintersectionr l r (union l' r')) (cons (dunionl (intersection l r) l' r') (cons (dunionr (intersection l r) l' r') nil)))).
   repeat apply prod_cons; try apply prod_nil; simpl; apply exist with (cons tt nil); intro req; destruct req; simpl; auto.
   generalize (eq_refl (union l' r')). generalize (eq_refl (intersection l r)). generalize (union l' r') at 2 3 4 5 6. generalize (intersection l r) at 2 3 4 5 6. intros t t' e e' R admits trans con' ass'. destruct con'; try (inversion e; inversion e'; fail); simpl in ass'.
    inversion e. clear e. subst. apply Exists_cons_hd. assumption.
    inversion e. clear e. subst. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
    inversion e'. clear e'. subst. apply Exists_cons_tl. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
    inversion e'. clear e'. subst. apply Exists_cons_tl. apply Exists_cons_tl. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
  apply existT2 with (cons (dintersectionl l r (class c t'1 t'2)) (cons (dintersectionr l r (class c t'1 t'2)) nil)).
   apply prod_cons; try apply prod_cons; try apply prod_nil; apply exist with (cons tt nil); intros req; destruct req; simpl; auto.
   generalize (eq_refl (class c t'1 t'2)). generalize (eq_refl (intersection l r)). generalize (class c t'1 t'2) at 2 3 4 5 6. generalize (intersection l r) at 2 3 4 5 6. intros t t' e e' R admits trans con' ass'. destruct con'; try (inversion e; inversion e'; fail).
    inversion e. subst. apply Exists_cons_hd. assumption.
    inversion e. subst. apply Exists_cons_tl. apply Exists_cons_hd. assumption.
 apply existT2 with (cons (dbottom _) nil).
  apply prod_cons; try apply prod_nil. apply exist with nil. intro req. destruct req.
  intros R admits trans con' ass'. apply Exists_cons_hd. intro req. destruct req.
 rename t1 into l. rename t2 into r. apply existT2 with (cons (dunion _ _ _) nil).
  apply prod_cons; try apply prod_nil. apply exist with (cons left (cons right nil)). intro req. destruct req; simpl; auto.
  generalize (eq_refl (union l r)). generalize (union l r) at 2 3 4 5 6. intros t e R admits trans con' ass'. apply Exists_cons_hd. intro req'. simpl in *. destruct con'; try (inversion e; fail); simpl in ass'.
   destruct req'; apply admits with (dtop _); intro req; destruct req.
   subst; destruct req'; apply (admits _ _ (dintersection _ _ _)); simpl; intro req; pose proof (ass' req) as ass'; destruct req; apply (fun d => trans _ _ _ _ d ass' (refl _)); ((apply proof with (dunionl _ _ _); simpl; intros _; apply refl) || (apply proof with (dunionr _ _ _); simpl; intros _; apply refl)).
   subst; destruct req'; apply (fun d d' => trans _ _ _ _ d (ass' tt) d'); ((apply proof with (dunionl _ _ _); simpl; intros _; apply refl) || (apply proof with (dunionr _ _ _); simpl; intros _; apply refl)).
   subst; destruct req'; apply (fun d d' => trans _ _ _ _ d (ass' tt) d'); ((apply proof with (dunionl _ _ _); simpl; intros _; apply refl) || (apply proof with (dunionr _ _ _); simpl; intros _; apply refl)).
   inversion e. clear e. subst. apply ass'.
 destruct t'; try (apply ftop || apply fintersection || apply fnone; intros t t' e e' con; destruct con; inversion e; inversion e'; fail).
  apply funion. intros t1' t2' e1 e2 con'. destruct con'; inversion e1; inversion e2; exact I.
  rename c0 into c'. pose proof (preinh_dec c c') as [ linh inh finite ]. apply existT2 with (in_map linh (fun t i => dclass c t1 t2 c' t'1 t'2 t (inh t i))).
   clear finite. induction linh; try apply prod_nil. apply prod_cons; try apply IHlinh. apply exist with (cons covariant (cons contravariant nil)). simpl. intro req. destruct req; auto.
   generalize (eq_refl (class c' t'1 t'2)). generalize (eq_refl (class c t1 t2)). generalize (class c' t'1 t'2) at 2 3 4 5 6. generalize (class c t1 t2) at 2 3 4 5 6. intros t t' e e' R admits trans con' ass'. destruct con'; try (inversion e; inversion e'; fail). inversion e. inversion e'. clear e e'. subst. pose proof (finite _ p) as finite. induction linh; [ destruct finite | ]. simpl in finite. pose proof (deq a c't) as deq. destruct deq as [ e | ne ].
    subst. apply Exists_cons_hd. simpl in *. assumption.
    apply Exists_cons_tl. apply IHlinh. destruct finite as [ e | finite ]; try assumption. destruct (ne e).
Qed.

Definition wf := wf.

End DDRule.
Import DDRule.

Module Decidable := Decidable T DRule ORule DDRule.
Definition Decidable := Decidable.Decidable.

Traditional/Declarative Subtyping

In reverse order for the paper, we now define traditional/declarative subtyping. The rules are specified just the same as the declarative ones, but with the expectation that the framework will add explicit reflexivity and transitvity rules to them (see Tradition.v). All in all, those rules formalize the declarative literal subtyping rules for Ceylon from Figure 10 in the paper, combined with the declarative subtyping rules for unions and intersections in Figure 1.

Module TRule <: Rules T.

Inductive TCon : T -> T -> Type
:= tparameter : TCon parameter parameter
 | ttop (t : T) : TCon t top
 | tintersectionl (l r : T) : TCon (intersection l r) l
 | tintersectionr (l r : T) : TCon (intersection l r) r
 | tintersection (t l r : T) : TCon t (intersection l r)
 | tbottom (t' : T) : TCon bottom t'
 | tunionl (l r : T) : TCon l (union l r)
 | tunionr (l r : T) : TCon r (union l r)
 | tunion (l r t' : T) : TCon (union l r) t'
 | tinherit (c : Class) (i o : T) (c' : Class) (c't : T) : pInh c c' c't -> TCon (class c i o) (class c' (fill o i c't) (fill i o c't))
 | tclass (c : Class) (i o i' o' : T) : TCon (class c i o) (class c i' o').
Local Definition Con := TCon.

Definition TReq {t t' : T} (con : Con t t')
:= match con in TCon t t' return Type with
   | tparameter => Empty
   | ttop _ => Empty
   | tintersectionl _ _ => Empty
   | tintersectionr _ _ => Empty
   | tintersection _ _ _ => Position
   | tbottom _ => Empty
   | tunionl _ _ => Empty
   | tunionr _ _ => Empty
   | tunion _ _ _ => Position
   | tinherit _ _ _ _ _ _ => Empty
   | tclass _ _ _ _ _ => Variance
   end.
Local Definition Req := @TReq.

Definition TAss {t t' : T} {con : Con t t'}
:= match con as con in TCon t t' return TReq con -> Position -> T with
   | tparameter => fun req => match req with end
   | ttop _ => fun req => match req with end
   | tintersectionl _ _ => fun req => match req with end
   | tintersectionr _ _ => fun req => match req with end
   | tintersection t l r => fun req pos => match req, pos with _, left => t | left, right => l | right, right => r end
   | tbottom _ => fun req => match req with end
   | tunionl _ _ => fun req => match req with end
   | tunionr _ _ => fun req => match req with end
   | tunion l r t' => fun req pos => match req, pos with _, right => t' | left, left => l | right, left => r end
   | tinherit c i o c' c't _ => fun req => match req with end
   | tclass c i o i' o' => fun req pos => match req, pos with
                                          | covariant, left => o
                                          | covariant, right => o'
                                          | contravariant, left => i'
                                          | contravariant, right => i
                                          end
   end.
Local Definition Ass := @TAss.

End TRule.
Import TRule.

Module Traditional := Traditional T TRule.

Translating Rules

Lastly, we need a way to translate between the traditional/declarative and the decidable/reductive subtyping rules. The two lemmas in this module are required by the framework, see Convert.v. This produces a proof that traditional/declarative and decidable/reductive subtyping in our system here are equivalent and decidable, just as in the end of Section 3 in the paper. The decidability result stems from decidable/reductive subtyping is decidable, see Decide.v.

Module CRule <: Converter T TRule DRule ORule DDRule.
Module Decidable := Decidable.
Module Basic := Proofs T TRule.
Module Traditional := Traditional.
Import Traditional.TransRefl.

Lemma decidable_traditional_R (R : T -> T -> Prop) : Traditional.Proof.Admits R -> Decidable.Proof.Admits R.
intro admits. intros t t' con ass. destruct con; simpl in ass.
 apply (admits _ _ (tcon tparameter)). intro req. destruct req.
 apply (admits _ _ (tcon (ttop _))). intro req. destruct req.
 apply (admits _ _ (trans _ l _)). simpl. intro req. destruct req.
  apply (admits _ _ (tcon (tintersectionl _ _))). intro req. destruct req.
  apply ass. constructor.
 apply (admits _ _ (trans _ r _)). simpl. intro req. destruct req.
  apply (admits _ _ (tcon (tintersectionr _ _))). intro req. destruct req.
  apply ass. constructor.
 apply (admits _ _ (tcon (tintersection _ _ _))). assumption.
 apply (admits _ _ (tcon (tbottom _))). intro req. destruct req.
 apply (admits _ _ (trans _ l _)). simpl. intro req. destruct req.
  apply ass. constructor.
  apply (admits _ _ (tcon (tunionl _ _))). intro req. destruct req.
 apply (admits _ _ (trans _ r _)). simpl. intro req. destruct req.
  apply ass. constructor.
  apply (admits _ _ (tcon (tunionr _ _))). intro req. destruct req.
 apply (admits _ _ (tcon (tunion _ _ _))). assumption.
 revert i o i' o' ass. induction p; intros i o i' o' ass.
  apply (admits _ _ (tcon (tclass _ _ _ _ _))). simpl. assumption.
  apply (admits _ _ (trans _ (class c' (fill o i c't) (fill i o c't)) _)). simpl. intros [ | ].
   apply (admits _ _ (tcon (tinherit _ _ _ _ _ H))). intros [].
   apply IHp. repeat rewrite <- fill_fill. assumption.
Qed.

Lemma traditional_decidable_R (R : T -> T -> Prop) : (forall t : T, R t t)
                                                  -> (forall t1 t2 t3 t4 : T, Decidable.Decidable t1 t2 -> R t2 t3 -> Decidable.Decidable t3 t4 -> R t1 t4)
                                                  -> Decidable.Proof.Admits R
                                                  -> Basic.Admits R.
intros refl trans admits. intros t t' con ass. destruct con; simpl in ass.
 apply (admits _ _ dparameter). intro req. destruct req.
 apply (admits _ _ (dtop _)). intro req. destruct req.
 apply (admits _ _ (dintersectionl _ _ _)). simpl. intros _. apply refl.
 apply (admits _ _ (dintersectionr _ _ _)). simpl. intros _. apply refl.
 apply (admits _ _ (dintersection _ _ _)). assumption.
 apply (admits _ _ (dbottom _)). intro req. destruct req.
 apply (admits _ _ (dunionl _ _ _)). simpl. intros _. apply refl.
 apply (admits _ _ (dunionr _ _ _)). simpl. intros _. apply refl.
 apply (admits _ _ (dunion _ _ _)). assumption.
 apply (admits _ _ (dclass _ _ _ _ _ _ _ (tinh _ _ _ _ _ p (rinh _)))). simpl. intro req. apply refl.
 apply (admits _ _ (dclass _ _ _ _ _ _ _ (rinh _))). assumption.
Qed.

End CRule.

Module Conversion := Conversion T TRule DRule ORule DDRule.

End Generics.

This page has been generated by coqdoc