Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
}.
Implicit Arguments ProofCaseBranch [ ].
-(* Figure 3, production $\vdash_E$, Uniform rules *)
-Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
-| RId : forall a , Arrange a a
-| RCanL : forall a , Arrange ( [],,a ) ( a )
-| RCanR : forall a , Arrange ( a,,[] ) ( a )
-| RuCanL : forall a , Arrange ( a ) ( [],,a )
-| RuCanR : forall a , Arrange ( a ) ( a,,[] )
-| RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
-| RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
-| RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
-| RWeak : forall a , Arrange ( [] ) ( a )
-| RCont : forall a , Arrange ( (a,,a) ) ( a )
-| RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
-| RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
-| RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
-.
-
(* Figure 3, production $\vdash_E$, all rules *)
Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ]
-(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l]
| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
+| RCut : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l]
+| RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
+
| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
Qed.
Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
auto.
Qed.
-(* "Arrange" objects are parametric in the type of the leaves of the tree *)
-Definition arrangeMap :
- forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
- Arrange Σ₁ Σ₂ ->
- Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
- intros.
- induction X; simpl.
- apply RId.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch.
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHX1 | apply IHX2 ].
- Defined.
-
-(* a frequently-used Arrange *)
-Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
- Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
- eapply RComp.
- apply RCossa.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
- eapply RAssoc.
- eapply RRight.
- apply RExch.
- eapply RComp.
- eapply RLeft.
- eapply RCossa.
- eapply RAssoc.
- Defined.