Library strip

Stripping functions

In this file, we describe how to get rid of the annotations introduced in PTSATR, to translate terms from PTSATR to PTS or PTSe.

Require Import base.

Require Import ut_term.

Require Import ut_red.

Require Import ut_env.

Require Import term.

Require Import env.

Require Import Peano_dec.

Require Import Compare_dec.

Require Import Lt.

Require Import List.

Module strip_mod (X:term_sig) (TM:ut_term_mod X) (T'M : term_mod X) (EM: ut_env_mod X TM) (E'M: env_mod X T'M).

Interactive Module strip_mod started

Import X TM T'M.

Open Scope Typ_scope.

Stripping function for terms and contexts.

strip is recursively defined (decreasing on 1st argument)

Fixpoint strip_env (Γ: E'M.Env) : EM.Env := match Γ with
| nil => nil
| A::Γ' => (strip A)::(strip_env Γ')
end.

strip_env is recursively defined (decreasing on 1st argument)

Stripping doesn't not mess with lift or subst .

Lemma strip_lift : forall M n m, strip (M ↑ n # m) = ((strip M ) ↑ n # m)%UT.

1 subgoals, subgoal 1 (ID 11)
  
  ============================
   forall (M : Term) (n m : nat), strip M ↑ n # m = ((strip M) ↑ n # m)%UT

(dependent evars:)

induction M; intros; simpl in *.

5 subgoals, subgoal 1 (ID 59)
  
  v : Vars
  n : nat
  m : nat
  ============================
   strip (if le_gt_dec m v then #(n + v) else #v) =
   (if le_gt_dec m v then #(n + v)%UT else #v%UT)

subgoal 2 (ID 63) is:
 !s%UT = !s%UT
subgoal 3 (ID 74) is:
 strip M1 ↑ n # m · strip M4 ↑ n # m =
 ((strip M1) ↑ n # m)%UT · ((strip M4) ↑ n # m)%UT
subgoal 4 (ID 81) is:
 (Π (strip (M1 ↑ n # m)%Typ), strip (M2 ↑ n # (S m))%Typ)%UT =
 (Π ((strip M1) ↑ n # m), (strip M2) ↑ n # (S m))%UT
subgoal 5 (ID 88) is:
 (λ [strip (M1 ↑ n # m)%Typ], strip (M2 ↑ n # (S m))%Typ)%UT =
 (λ [(strip M1) ↑ n # m], (strip M2) ↑ n # (S m))%UT
(dependent evars:)

destruct le_gt_dec; simpl; trivial.

4 subgoals, subgoal 1 (ID 63)
  
  s : Sorts
  n : nat
  m : nat
  ============================
   !s%UT = !s%UT

subgoal 2 (ID 74) is:
 strip M1 ↑ n # m · strip M4 ↑ n # m =
 ((strip M1) ↑ n # m)%UT · ((strip M4) ↑ n # m)%UT
subgoal 3 (ID 81) is:
 (Π (strip (M1 ↑ n # m)%Typ), strip (M2 ↑ n # (S m))%Typ)%UT =
 (Π ((strip M1) ↑ n # m), (strip M2) ↑ n # (S m))%UT
subgoal 4 (ID 88) is:
 (λ [strip (M1 ↑ n # m)%Typ], strip (M2 ↑ n # (S m))%Typ)%UT =
 (λ [(strip M1) ↑ n # m], (strip M2) ↑ n # (S m))%UT
(dependent evars:)

trivial.

3 subgoals, subgoal 1 (ID 74)
  
  M1 : Term
  M2 : Term
  M3 : Term
  M4 : Term
  IHM1 : forall n m : nat, strip M1 ↑ n # m = ((strip M1) ↑ n # m)%UT
  IHM2 : forall n m : nat, strip M2 ↑ n # m = ((strip M2) ↑ n # m)%UT
  IHM3 : forall n m : nat, strip M3 ↑ n # m = ((strip M3) ↑ n # m)%UT
  IHM4 : forall n m : nat, strip M4 ↑ n # m = ((strip M4) ↑ n # m)%UT
  n : nat
  m : nat
  ============================
   strip M1 ↑ n # m · strip M4 ↑ n # m =
   ((strip M1) ↑ n # m)%UT · ((strip M4) ↑ n # m)%UT

subgoal 2 (ID 81) is:
 (Π (strip (M1 ↑ n # m)%Typ), strip (M2 ↑ n # (S m))%Typ)%UT =
 (Π ((strip M1) ↑ n # m), (strip M2) ↑ n # (S m))%UT
subgoal 3 (ID 88) is:
 (λ [strip (M1 ↑ n # m)%Typ], strip (M2 ↑ n # (S m))%Typ)%UT =
 (λ [(strip M1) ↑ n # m], (strip M2) ↑ n # (S m))%UT
(dependent evars:)

rewrite IHM1, IHM4; trivial.

2 subgoals, subgoal 1 (ID 81)
  
  M1 : Term
  M2 : Term
  IHM1 : forall n m : nat, strip M1 ↑ n # m = ((strip M1) ↑ n # m)%UT
  IHM2 : forall n m : nat, strip M2 ↑ n # m = ((strip M2) ↑ n # m)%UT
  n : nat
  m : nat
  ============================
   (Π (strip (M1 ↑ n # m)%Typ), strip (M2 ↑ n # (S m))%Typ)%UT =
   (Π ((strip M1) ↑ n # m), (strip M2) ↑ n # (S m))%UT

subgoal 2 (ID 88) is:
 (λ [strip (M1 ↑ n # m)%Typ], strip (M2 ↑ n # (S m))%Typ)%UT =
 (λ [(strip M1) ↑ n # m], (strip M2) ↑ n # (S m))%UT
(dependent evars:)

rewrite IHM1, IHM2; trivial.

1 subgoals, subgoal 1 (ID 88)
  
  M1 : Term
  M2 : Term
  IHM1 : forall n m : nat, strip M1 ↑ n # m = ((strip M1) ↑ n # m)%UT
  IHM2 : forall n m : nat, strip M2 ↑ n # m = ((strip M2) ↑ n # m)%UT
  n : nat
  m : nat
  ============================
   (λ [strip (M1 ↑ n # m)%Typ], strip (M2 ↑ n # (S m))%Typ)%UT =
   (λ [(strip M1) ↑ n # m], (strip M2) ↑ n # (S m))%UT

(dependent evars:)

rewrite IHM1, IHM2; trivial.

No more subgoals.
(dependent evars:)

Qed.

strip_lift is defined

Lemma strip_subst : forall M n N, strip (M [n ← N ]) = ((strip M ) [ n ← strip N ])%UT.

1 subgoals, subgoal 1 (ID 115)
  
  ============================
   forall (M : Term) (n : nat) (N : Term),
   strip M [n ← N] = ((strip M) [n ← strip N])%UT

(dependent evars:)

induction M; intros; simpl in *.

5 subgoals, subgoal 1 (ID 163)
  
  v : Vars
  n : nat
  N : Term
  ============================
   strip
     match lt_eq_lt_dec v n with
     | inleft (left _) => #v
     | inleft (right _) => N ↑ n
     | inright _ => #(v - 1)
     end =
   match lt_eq_lt_dec v n with
   | inleft (left _) => #v%UT
   | inleft (right _) => ((strip N) ↑ n)%UT
   | inright _ => #(v - 1)%UT
   end

subgoal 2 (ID 167) is:
 !s%UT = !s%UT
subgoal 3 (ID 178) is:
 strip M1 [n ← N] · strip M4 [n ← N] =
 ((strip M1) [n ← strip N])%UT · ((strip M4) [n ← strip N])%UT
subgoal 4 (ID 185) is:
 (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
 (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT
subgoal 5 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

destruct lt_eq_lt_dec as [ [] | ]; simpl; trivial.

5 subgoals, subgoal 1 (ID 210)
  
  v : Vars
  n : nat
  N : Term
  e : v = n
  ============================
   strip N ↑ n = ((strip N) ↑ n)%UT

subgoal 2 (ID 167) is:
 !s%UT = !s%UT
subgoal 3 (ID 178) is:
 strip M1 [n ← N] · strip M4 [n ← N] =
 ((strip M1) [n ← strip N])%UT · ((strip M4) [n ← strip N])%UT
subgoal 4 (ID 185) is:
 (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
 (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT
subgoal 5 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

rewrite strip_lift.

5 subgoals, subgoal 1 (ID 212)
  
  v : Vars
  n : nat
  N : Term
  e : v = n
  ============================
   ((strip N) ↑ n)%UT = ((strip N) ↑ n)%UT

subgoal 2 (ID 167) is:
 !s%UT = !s%UT
subgoal 3 (ID 178) is:
 strip M1 [n ← N] · strip M4 [n ← N] =
 ((strip M1) [n ← strip N])%UT · ((strip M4) [n ← strip N])%UT
subgoal 4 (ID 185) is:
 (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
 (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT
subgoal 5 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

trivial.

4 subgoals, subgoal 1 (ID 167)
  
  s : Sorts
  n : nat
  N : Term
  ============================
   !s%UT = !s%UT

subgoal 2 (ID 178) is:
 strip M1 [n ← N] · strip M4 [n ← N] =
 ((strip M1) [n ← strip N])%UT · ((strip M4) [n ← strip N])%UT
subgoal 3 (ID 185) is:
 (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
 (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT
subgoal 4 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

trivial.

3 subgoals, subgoal 1 (ID 178)
  
  M1 : Term
  M2 : Term
  M3 : Term
  M4 : Term
  IHM1 : forall (n : nat) (N : Term),
         strip M1 [n ← N] = ((strip M1) [n ← strip N])%UT
  IHM2 : forall (n : nat) (N : Term),
         strip M2 [n ← N] = ((strip M2) [n ← strip N])%UT
  IHM3 : forall (n : nat) (N : Term),
         strip M3 [n ← N] = ((strip M3) [n ← strip N])%UT
  IHM4 : forall (n : nat) (N : Term),
         strip M4 [n ← N] = ((strip M4) [n ← strip N])%UT
  n : nat
  N : Term
  ============================
   strip M1 [n ← N] · strip M4 [n ← N] =
   ((strip M1) [n ← strip N])%UT · ((strip M4) [n ← strip N])%UT

subgoal 2 (ID 185) is:
 (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
 (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT
subgoal 3 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

rewrite IHM1, IHM4; trivial.

2 subgoals, subgoal 1 (ID 185)
  
  M1 : Term
  M2 : Term
  IHM1 : forall (n : nat) (N : Term),
         strip M1 [n ← N] = ((strip M1) [n ← strip N])%UT
  IHM2 : forall (n : nat) (N : Term),
         strip M2 [n ← N] = ((strip M2) [n ← strip N])%UT
  n : nat
  N : Term
  ============================
   (Π (strip (M1 [n ← N])%Typ), strip (M2 [(S n) ← N])%Typ)%UT =
   (Π ((strip M1) [n ← strip N]), (strip M2) [(S n) ← strip N])%UT

subgoal 2 (ID 192) is:
 (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
 (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT
(dependent evars:)

rewrite IHM1, IHM2; trivial.

1 subgoals, subgoal 1 (ID 192)
  
  M1 : Term
  M2 : Term
  IHM1 : forall (n : nat) (N : Term),
         strip M1 [n ← N] = ((strip M1) [n ← strip N])%UT
  IHM2 : forall (n : nat) (N : Term),
         strip M2 [n ← N] = ((strip M2) [n ← strip N])%UT
  n : nat
  N : Term
  ============================
   (λ [strip (M1 [n ← N])%Typ], strip (M2 [(S n) ← N])%Typ)%UT =
   (λ [(strip M1) [n ← strip N]], (strip M2) [(S n) ← strip N])%UT

(dependent evars:)

rewrite IHM1, IHM2; trivial.

No more subgoals.
(dependent evars:)

Qed.

strip_subst is defined

End strip_mod.

Module strip_mod is defined

Index

This page has been generated by coqdoc