some cosmetics

subterm.v

@@ -1,8 +1,9 @@
 Require Import MetaCoq.Template.All.
-Require Import List String.
-Require Import Coq.Program.Equality.
+Require Import List String Relation_Operators.
 Import ListNotations MonadNotation.
 
+(* Require Import sigma. *)
+
 Definition filteri {A: Type} (f : nat -> A -> bool) (l:list A) : list A :=
   let go := fix go n l := match l with
                          | nil => nil
@@ -19,8 +20,8 @@ Definition opt_nil {A : Type} (x : option A) : list A := match x with Some a =>
 Definition clift0 (n : nat) (t : context_decl) : context_decl :=
   {| decl_name := t.(decl_name);
      decl_body := match t.(decl_body) with
-                  | Some q => Some (lift0 n q)
-                  | None => None
+                   | Some q => Some (lift0 n q)
+                   | None => None
                   end;
      decl_type := lift0 n t.(decl_type)
   |}.
@@ -86,10 +87,12 @@ Definition subterm_for_ind
   := let (pai, sort) := decompose_prod_assum [] ind.(ind_type) in
      let inds := List.firstn (List.length pai - npars) pai in
      let leni := List.length inds in
-     let aptype1 := tApp ref ((map (lift0 (2 * leni)) (to_extended_list pars)) ++
-                              (map (lift0 leni) (to_extended_list inds))) in
-     let aptype2 := tApp ref ((map (lift0 (1 + 2 * leni)) (to_extended_list pars)) ++
-                              (map (lift0 1) (to_extended_list inds))) in
+     let aptype1 :=
+         tApp ref ((map (lift0 (2 * leni)) (to_extended_list pars)) ++
+                   (map (lift0 leni) (to_extended_list inds))) in
+     let aptype2 :=
+         tApp ref ((map (lift0 (1 + 2 * leni)) (to_extended_list pars)) ++
+                   (map (lift0 1) (to_extended_list inds))) in
      let renamer name i := (name ++ "_subterm" ++ (string_of_nat i))%string in
      {| ind_name := (ind.(ind_name) ++ "_direct_subterm")%string;
         (* type_for_direct_subterm npars *)
@@ -107,7 +110,7 @@ Definition subterm_for_ind
                         ind.(ind_ctors));
         ind_projs := [] |}.
 
-Definition subterm_for_mutual_ind
+Definition direct_subterm_for_mutual_ind
             (mind : mutual_inductive_body)
             (ind0 : inductive) (* internal metacoq representation of inductive, part of tInd *)
             (ref  : term) (* reference term for the inductive type, like (tInd {| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} []) *)
@@ -123,31 +126,46 @@ Definition subterm_for_mutual_ind
                       mind.(ind_bodies);
      |}.
 
-Inductive nnat (A : Type) : Type :=
-  n_zero : nnat A
-| n_one : (nat -> nnat (list A)) -> nnat A.
-
 Polymorphic Definition subterm (tm : Ast.term)
   : TemplateMonad unit
   := match tm with
      | tInd ind0 _ =>
        (* ge_ <- tmQuoteRec tm;; *)
        decl <- tmQuoteInductive (inductive_mind ind0);;
-       let subt := subterm_for_mutual_ind decl ind0 tm in
-       v <- tmEval cbv subt;;
-       tmPrint v;;
-       (* tmPrint (print_term (fst ge_, decl.(ind_universes)) [] true v) *)
-       tmMkInductive' v
+       let direct_subterm := direct_subterm_for_mutual_ind decl ind0 tm in
+       tmMkInductive' direct_subterm
+       (* v <- tmEval direct_subterm;;
+          tmPrint v;; *)
      | _ => tmPrint tm;; tmFail "is not an inductive"
      end.
 
-
 Inductive finn (A : Type) : nat -> Set :=
   F1n : forall n : nat, finn A (S n)
 | FSn : forall n : nat, finn A n -> finn A (S n).
 
-Inductive fin : nat -> Set :=
-  F1 : forall n : nat, fin (S n)
+Inductive fin : nat -> Type :=
+  F1 : forall n : nat, fin (let x := S n in x)
 | FS : forall n : nat, fin n -> fin (S n).
 
-Run TemplateProgram (subterm <%finn%>).
+Run TemplateProgram (subterm <%list%>).
+Print list_direct_subterm.
+
+Definition scope := nat.
+Inductive scope_le : scope -> scope -> Set :=
+| scope_le_n : forall {n m}, n = m -> scope_le n m
+| scope_le_S : forall {n m}, scope_le n m -> scope_le n (S m)
+| scope_le_map : forall {n m}, scope_le n m -> scope_le (S n) (S m)
+.
+
+Run TemplateProgram (subterm <%scope_le%>).
+
+(*
+Inductive
+scope_le_direct_subterm
+    : forall H H0 H1 H2 : scope, scope_le H H0 -> scope_le H1 H2 -> Set :=
+    scope_le_S_subterm0 : forall (n m : scope) (H : scope_le n m),
+                          scope_le_direct_subterm n m n (S m) H (scope_le_S H)
+  | scope_le_map_subterm0 : forall (n m : scope) (H : scope_le n m),
+                            scope_le_direct_subterm n m 
+                              (S n) (S m) H (scope_le_map H)
+*)