Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import HaskKinds.
Require Import HaskLiterals.
Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
*)
Section HaskFlattener.
- Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
- match lht with t @@ l => l end.
-
- Definition arrange :
- forall {T} (Σ:Tree ??T) (f:T -> bool),
- Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
- intros.
- induction Σ.
- simpl.
- destruct a.
- simpl.
- destruct (f t); simpl.
- apply RuCanL.
- apply RuCanR.
- simpl.
- apply RuCanL.
- simpl in *.
- eapply RComp; [ idtac | apply arrangeSwapMiddle ].
- eapply RComp.
- eapply RLeft.
- apply IHΣ2.
- eapply RRight.
- apply IHΣ1.
- Defined.
-
- Definition arrange' :
- forall {T} (Σ:Tree ??T) (f:T -> bool),
- Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
- intros.
- induction Σ.
- simpl.
- destruct a.
- simpl.
- destruct (f t); simpl.
- apply RCanL.
- apply RCanR.
- simpl.
- apply RCanL.
- simpl in *.
- eapply RComp; [ apply arrangeSwapMiddle | idtac ].
- eapply RComp.
- eapply RLeft.
- apply IHΣ2.
- eapply RRight.
- apply IHΣ1.
- Defined.
Ltac eqd_dec_refl' :=
match goal with
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 :=
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.
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.
Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskProof.
Section HaskStrongToProof.
-
-Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
- RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
-
-Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
- RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
-
-Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
- eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
- eapply RComp; [ idtac | apply RCossa ].
- eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
- apply RAssoc.
- Defined.
-
+
Context {VV:Type}{eqd_vv:EqDecidable VV}.
(* maintenance of Xi *)
--- /dev/null
+(*********************************************************************************************************************************)
+(* NaturalDeductionContext: *)
+(* *)
+(* Manipulations of a context in natural deduction proofs. *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+
+Section NaturalDeductionContext.
+
+ (* 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
+ .
+
+ (* "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.
+
+ Definition arrange :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply RuCanL.
+ apply RuCanR.
+ simpl.
+ apply RuCanL.
+ simpl in *.
+ eapply RComp; [ idtac | apply arrangeSwapMiddle ].
+ eapply RComp.
+ eapply RLeft.
+ apply IHΣ2.
+ eapply RRight.
+ apply IHΣ1.
+ Defined.
+
+ Definition arrange' :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply RCanL.
+ apply RCanR.
+ simpl.
+ apply RCanL.
+ simpl in *.
+ eapply RComp; [ apply arrangeSwapMiddle | idtac ].
+ eapply RComp.
+ eapply RLeft.
+ apply IHΣ2.
+ eapply RRight.
+ apply IHΣ1.
+ Defined.
+
+ Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+ RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+
+ Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
+ RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
+
+ Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
+ eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
+ eapply RComp; [ idtac | apply RCossa ].
+ eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
+ apply RAssoc.
+ Defined.
+
+End NaturalDeductionContext.