adam@1618: (* Copyright (c) 2009, 2011, Adam Chlipala
adamc@615:  * All rights reserved.
adamc@615:  *
adamc@615:  * Redistribution and use in source and binary forms, with or without
adamc@615:  * modification, are permitted provided that the following conditions are met:
adamc@615:  *
adamc@615:  * - Redistributions of source code must retain the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer.
adamc@615:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer in the documentation
adamc@615:  *   and/or other materials provided with the distribution.
adamc@615:  * - The names of contributors may not be used to endorse or promote products
adamc@615:  *   derived from this software without specific prior written permission.
adamc@615:  *
adamc@615:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@615:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@615:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@615:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@615:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@615:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@615:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@615:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@615:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@615:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@615:  * POSSIBILITY OF SUCH DAMAGE.
adamc@615:  *)
adamc@615: 
adam@1618: Require Import Eqdep_dec.
adamc@618: 
adamc@616: Require Import Axioms.
adamc@615: Require Import Syntax.
adamc@615: 
adamc@615: Set Implicit Arguments.
adamc@615: 
adamc@615: 
adamc@617: Definition row (A : Type) : Type := name -> option A.
adamc@615: 
adamc@617: Definition record (r : row Set) := forall n, match r n with
adamc@617:                                                | None => unit
adamc@617:                                                | Some T => T
adamc@617:                                              end.
adamc@615: 
adamc@615: Fixpoint kDen (k : kind) : Type :=
adamc@615:   match k with
adamc@615:     | KType => Set
adamc@615:     | KName => name
adamc@615:     | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615:     | KRecord k1 => row (kDen k1)
adamc@615:   end.
adamc@615: 
adamc@635: Definition disjoint T (r1 r2 : row T) :=
adamc@635:   forall n, match r1 n, r2 n with
adamc@635:               | Some _, Some _ => False
adamc@635:               | _, _ => True
adamc@635:             end.
adamc@620: 
adam@1618: Fixpoint cDen k (c : con kDen k) : kDen k :=
adam@1618:   match c with
adamc@615:     | CVar _ x => x
adamc@615:     | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615:     | Poly _ c1 => forall x, cDen (c1 x)
adamc@615:     | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615:     | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615:     | Name n => n
adamc@615:     | TRecord c1 => record (cDen c1)
adamc@617:     | CEmpty _ => fun _ => None
adamc@617:     | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
adamc@617:     | CConcat _ c1 c2 => fun n => match (cDen c1) n with
adamc@617:                                     | None => (cDen c2) n
adamc@617:                                     | v => v
adamc@617:                                   end
adamc@617:     | CMap k1 k2 => fun f r n => match r n with
adamc@617:                                    | None => None
adamc@617:                                    | Some T => Some (f T)
adamc@617:                                  end
adamc@635:     | TGuarded _ c1 c2 t => disjoint (cDen c1) (cDen c2) -> cDen t
adamc@615:   end.
adamc@616: 
adamc@616: Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616:   subs c1 c2 c2'
adamc@616:   -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616:   induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616:     repeat match goal with
adamc@616:              | [ H : _ |- _ ] => rewrite H
adamc@616:            end; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
adamc@616:   disjoint (cDen c1) (cDen c2).
adamc@616: 
adamc@616: Scheme deq_mut := Minimality for deq Sort Prop
adamc@616: with disj_mut := Minimality for disj Sort Prop.
adamc@616: 
adamc@618: Ltac deq_disj_correct scm :=
adamc@635:   let t := repeat progress (simpl; intuition; subst) in
adamc@617: 
adamc@618:   let rec use_disjoint' notDone E :=
adamc@617:     match goal with
adamc@617:       | [ H : disjoint _ _ |- _ ] =>
adamc@617:         notDone H; generalize (H E); use_disjoint'
adamc@617:           ltac:(fun H' =>
adamc@617:             match H' with
adamc@617:               | H => fail 1
adamc@617:               | _ => notDone H'
adamc@617:             end) E
adamc@617:       | _ => idtac
adamc@618:     end in
adamc@618:   let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in
adamc@616: 
adamc@618:   apply (scm _ dvar
adamc@616:     (fun k (c1 c2 : con kDen k) =>
adamc@616:       cDen c1 = cDen c2)
adamc@616:     (fun k (c1 c2 : con kDen (KRecord k)) =>
adamc@617:       disjoint (cDen c1) (cDen c2))); t;
adamc@617:   repeat ((unfold row; apply ext_eq)
adamc@617:     || (match goal with
adamc@620:           | [ H : _ |- _ ] => rewrite H; []
adamc@617:           | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
adamc@617:         end); t);
adamc@617:   unfold disjoint; t;
adamc@616:     repeat (match goal with
adamc@617:               | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
adamc@617:                 use_disjoint E; destruct (cDen C E)
adamc@617:               | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
adamc@617:                 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
adamc@617:               | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
adamc@617:                 use_disjoint E; destruct (cDen C E)
adamc@620:               | [ |- context[if ?E then _ else _] ] => destruct E                  
adamc@617:             end; t).
adamc@618: 
adamc@620: Hint Unfold dvar.
adamc@620: 
adamc@618: Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@618:   deq dvar c1 c2
adamc@618:   -> cDen c1 = cDen c2.
adamc@618:   deq_disj_correct deq_mut.
adamc@616: Qed.
adamc@618: 
adamc@618: Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
adamc@618:   disj dvar c1 c2
adamc@618:   -> disjoint (cDen c1) (cDen c2).
adamc@618:   deq_disj_correct disj_mut.
adamc@618: Qed.
adamc@618: 
adamc@618: Definition tDen (t : con kDen KType) : Set := cDen t.
adamc@618: 
adamc@618: Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
adamc@618:   intros; destruct (name_eq_dec n n); intuition; [
adamc@618:     match goal with
adam@1618:       | [ e : _ = _ |- _ ] => rewrite (UIP_dec name_eq_dec e (refl_equal _)); reflexivity
adamc@618:     end
adamc@618:     | elimtype False; tauto
adamc@618:   ].
adamc@618: Qed.
adamc@618: 
adamc@618: Theorem cut_disjoint : forall n1 v r,
adamc@618:   disjoint (fun n => if name_eq_dec n n1 then Some v else None) r
adamc@618:   -> unit = match r n1 with
adamc@618:               | Some T => T
adamc@618:               | None => unit
adamc@618:             end.
adamc@618:   intros;
adamc@618:     match goal with
adamc@618:       | [ H : disjoint _ _ |- _ ] => generalize (H n1)
adamc@618:     end; rewrite name_eq_dec_refl;
adamc@618:     destruct (r n1); intuition.
adamc@618: Qed.
adamc@618: 
adamc@618: Implicit Arguments cut_disjoint [v r].
adamc@618: 
adam@1618: Fixpoint eDen t (e : exp dvar tDen t) : tDen t :=
adamc@618:   match e in exp _ _ t return tDen t with
adamc@618:     | Var _ x => x
adamc@618:     | App _ _ e1 e2 => (eDen e1) (eDen e2)
adamc@618:     | Abs _ _ e1 => fun x => eDen (e1 x)
adamc@618:     | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
adamc@618:                                  | refl_equal => (eDen e1) (cDen c)
adamc@618:                                end
adamc@618:     | ECAbs _ _ e1 => fun X => eDen (e1 X)
adamc@618:     | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
adamc@618:                            | refl_equal => eDen e1
adamc@618:                          end
adamc@618:     | Empty => fun _ => tt
adam@1618:     | Single c c' e1 => fun n => if name_eq_dec n (cDen c) as B
adam@1618:       return (match (match (if B then _ else _) with Some _ => _ | None => _ end)
adamc@618:                 with Some _ => _ | None => unit end)
adamc@618:       then eDen e1 else tt
adamc@618:     | Proj c _ _ e1 =>
adamc@618:       match name_eq_dec_refl (cDen c) in _ = B
adamc@618:         return (match (match (if B then _ else _) with
adam@1618:                          | Some _ => _
adamc@618:                          | None => _ end)
adamc@618:         return Set
adamc@618:                   with Some _ => _ | None => _ end) with
adamc@618:         | refl_equal => (eDen e1) (cDen c)
adamc@618:       end
adamc@618:     | Cut c _ c' Hdisj e1 => fun n =>
adam@1618:       match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => _ | None => (cDen c') n end)
adamc@618:                                                   with Some T => T | None => unit end
adamc@618:       -> match (cDen c') n with
adamc@618:            | None => unit
adamc@618:            | Some T => T
adamc@618:          end) with 
adamc@618:         | left Heq => fun _ =>
adamc@618:           match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with
adamc@618:             | refl_equal =>
adamc@618:               match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with
adamc@618:                 | refl_equal => tt
adamc@618:               end
adamc@618:           end
adamc@618:         | right _ => fun x => x
adamc@618:       end ((eDen e1) n)
adamc@618: 
adamc@619:     | Concat c1 c2 e1 e2 => fun n =>
adamc@619:       match (cDen c1) n as D return match D with
adamc@619:                                       | None => unit
adamc@619:                                       | Some T => T
adamc@619:                                     end
adamc@619:       -> match (match D with
adamc@619:                   | None => (cDen c2) n
adam@1618:                   | Some v => Some v
adamc@619:                 end) with
adamc@619:            | None => unit
adamc@619:            | Some T => T
adamc@619:          end with
adamc@619:         | None => fun _ => (eDen e2) n
adamc@619:         | _ => fun x => x
adamc@619:       end ((eDen e1) n)
adamc@619: 
adamc@635:     | Guarded _ _ _ _ e1 => fun pf => eDen (e1 pf)
adamc@635:     | GuardedApp _ _ _ _ e1 Hdisj => (eDen e1) (disj_correct Hdisj)
adamc@618:   end.