Temporary fix to #58

plugin/coq/TestLift.v

@@ -39,10 +39,7 @@ Proof.
   intros. reflexivity.
 Qed.
 
-Definition consV' (A : Type) (a : A) (pv : sigT (vector A)) :=
-  existT (vector A) (S (projT1 pv)) (consV A (projT1 pv) a (projT2 pv)).
-
-Lift vector list in consV' as consV'_c.
+Lift vector list in cons'_c as consV'_c.
 Theorem testConsV:
   forall A a l,
     consV'_c A a l = @cons A a l.
@@ -79,7 +76,7 @@ Proof.
   intros. reflexivity.
 Qed.
 
-Lift vector list in hd_vect as hd_lifted.
+Lift vector list in hd_vect_lifted as hd_lifted.
 
 Theorem test_hd:
   forall (A : Type) (default : A) (l : list A),
@@ -117,7 +114,7 @@ Proof.
   intros. reflexivity.
 Qed.
 
-Lift orn_flist_flector_nat_inv orn_flist_flector_nat in hd_vectF as hdF_lifted.
+Lift orn_flist_flector_nat_inv orn_flist_flector_nat in hd_vectF_lifted as hdF_lifted.
 
 Theorem test_hdF:
   forall (default : nat) (l : natFlector.flist),
@@ -155,7 +152,7 @@ Proof.
   intros. reflexivity.
 Qed.
 
-Lift vector list in hd_vect_error as hd_error_lifted.
+Lift vector list in hd_vect_error_lifted as hd_error_lifted.
 
 Theorem test_hd_error:
   forall (A : Type) (l : list A),
@@ -179,8 +176,6 @@ Definition append (A : Type) (l1 : list A) (l2 : list A) :=
       a :: IH)
     l1.
 
-
-
 Definition append_vect_inner (A : Type) (pv1 : sigT (vector A)) (pv2 : sigT (vector A)) :=
   vector_rect
     A
@@ -206,8 +201,7 @@ Proof.
   intros. reflexivity.
 Qed.
 
-Lift vector list in append_vect_inner as append_lifted_inner.
-Lift vector list in append_vect as append_lifted.
+Lift vector list in append_vect_lifted as append_lifted.
 
 Theorem test_append :
   forall (A : Type) (l1 : list A) (l2 : list A),

plugin/src/automation/lift.ml

@@ -524,11 +524,15 @@ let lift_core env evd c ib_typ trm =
            mkLambda (n, t', b'), false
         | LetIn (n, trm, typ, e) ->
            (* LETIN *)
-           let trm' = lift_rec en ib_typ trm in
-           let typ' = lift_rec en ib_typ typ in
-           let en_e = push_let_in (n, trm, typ) en in
-           let e' = lift_rec en_e (shift ib_typ) e in
-           mkLetIn (n, trm', typ', e'), false
+           if l.is_fwd then
+             let trm' = lift_rec en ib_typ trm in
+             let typ' = lift_rec en ib_typ typ in
+             let en_e = push_let_in (n, trm, typ) en in
+             let e' = lift_rec en_e (shift ib_typ) e in
+             mkLetIn (n, trm', typ', e'), false
+           else
+             (* Needed for #58 we implement #42 *)
+             lift_rec en ib_typ (whd en evd tr), false
         | Case (ci, ct, m, bs) ->
            (* CASE (will not work if this destructs over A; preprocess first) *)
            let ct' = lift_rec en ib_typ ct in
@@ -592,7 +596,7 @@ let lift_core env evd c ib_typ trm =
 let do_lift_term env evd (l : lifting) trm =
   let (a_t, b_t, i_b_t) = typs_from_orn l env evd in
   let c = initialize_lift_config env evd l (a_t, b_t) in
-  lift_core env evd c i_b_t trm
+  lift_core env evd c i_b_t (trm )
 
 (*
  * Run the core lifting algorithm on a definition

plugin/src/lib/coqterms.ml

@@ -447,6 +447,12 @@ let delta (env : env) (trm : types) =
     Evd.empty
     (Reductionops.whd_delta env Evd.empty (EConstr.of_constr trm))
 
+(* Weak head reduction *)
+let whd (env : env) (sigma : evar_map) (trm : types) : types =
+  EConstr.to_constr
+    sigma
+    (Reductionops.whd_all env sigma (EConstr.of_constr trm))
+
 (*
  * There's a part of the env that has opacity info,
  * so if you want to make some things opaque, can add them

plugin/src/lib/coqterms.mli

@@ -511,6 +511,7 @@ val convertible : env -> types -> types -> bool
 val reduce_term : env -> types -> types (* betaiotazeta *)
 val delta : env -> types -> types (* delta *)
 val reduce_nf : env -> types ->  types (* nf_all *)
+val whd : env -> evar_map -> types -> types (* whd_all *)
 val reduce_type : env -> evar_map -> types -> types (* betaiotazeta on types *)
 val chain_reduce : (* sequencing *)
   (env -> types -> types) ->