From 1cd3dd6abe296e1aedacd7e714702d13ffc156e5 Mon Sep 17 00:00:00 2001 From: Meven Date: Mon, 21 Aug 2023 17:31:05 +0100 Subject: [PATCH] remove useless bind with id --- theories/Decidability/Completeness.v | 2 +- theories/Decidability/Functions.v | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/theories/Decidability/Completeness.v b/theories/Decidability/Completeness.v index aa21b4a..2deca97 100644 --- a/theories/Decidability/Completeness.v +++ b/theories/Decidability/Completeness.v @@ -629,7 +629,7 @@ Proof. all: unfold graph in *. all: simp typing typing_inf typing_wf_ty typing_inf_red typing_check ; cbn. (* Well formed types *) - 1-5:repeat match goal with | |- orec_graph typing _ _ => econstructor ; try eauto ; cbn end. + 1-5:repeat match goal with | |- orec_graph typing _ _ => patch_rec_ret ; econstructor ; try eauto ; cbn end. - cbn in *. econstructor. 1: exact (g1 tt). diff --git a/theories/Decidability/Functions.v b/theories/Decidability/Functions.v index f0207fc..8be02fa 100644 --- a/theories/Decidability/Functions.v +++ b/theories/Decidability/Functions.v @@ -169,20 +169,20 @@ Arguments rec {_ _ _ _ _ _}. Equations wh_red_stack : term × stack ⇀[empty_store] term := wh_red_stack (t,π) with (build_tm_view1 t) := wh_red_stack (?(tRel n) ,π) (tm_view1_rel n) := ret (zip (tRel n) π) ; - wh_red_stack (?(zip1 t s) ,π) (tm_view1_dest t s) := id <*> rec (t,cons s π) ; + wh_red_stack (?(zip1 t s) ,π) (tm_view1_dest t s) := rec (t,cons s π) ; wh_red_stack (?(tLambda A t) ,nil) (tm_view1_fun A t) := ret (tLambda A t) ; - wh_red_stack (?(tLambda A t) ,cons (eApp u) π) (tm_view1_fun A t) := id <*> rec (t[u..], π) ; + wh_red_stack (?(tLambda A t) ,cons (eApp u) π) (tm_view1_fun A t) := rec (t[u..], π) ; wh_red_stack (_ ,cons _ _) (tm_view1_fun _ _) := undefined ; wh_red_stack (t ,nil) (tm_view1_nat _) := ret t ; - wh_red_stack (?(tZero) ,cons (eNatElim _ hz _) π) (tm_view1_nat eZero) := id <*> rec (hz,π) ; - wh_red_stack (?(tSucc t) ,cons (eNatElim P hz hs) π) (tm_view1_nat (eSucc t)) := id <*> rec (hs ,cons (eApp t) (cons (eApp (tNatElim P hz hs t)) π)) ; + wh_red_stack (?(tZero) ,cons (eNatElim _ hz _) π) (tm_view1_nat eZero) := rec (hz,π) ; + wh_red_stack (?(tSucc t) ,cons (eNatElim P hz hs) π) (tm_view1_nat (eSucc t)) := rec (hs ,cons (eApp t) (cons (eApp (tNatElim P hz hs t)) π)) ; wh_red_stack (t ,cons _ _) (tm_view1_nat _) := undefined ; wh_red_stack (?(tPair A B a b),nil) (tm_view1_sig A B a b) := ret (tPair A B a b) ; - wh_red_stack (?(tPair A B a b),cons eFst π) (tm_view1_sig A B a b) := id <*> rec (a , π) ; - wh_red_stack (?(tPair A B a b),cons eSnd π) (tm_view1_sig A B a b) := id <*> rec (b , π) ; + wh_red_stack (?(tPair A B a b),cons eFst π) (tm_view1_sig A B a b) := rec (a , π) ; + wh_red_stack (?(tPair A B a b),cons eSnd π) (tm_view1_sig A B a b) := rec (b , π) ; wh_red_stack (?(tPair A B a b),cons _ π) (tm_view1_sig A B a b) := undefined ; wh_red_stack (?(tRefl A x) ,nil) (tm_view1_id A x) := ret (tRefl A x) ; - wh_red_stack (?(tRefl A x) ,cons (eIdElim _ _ _ hr _) π) (tm_view1_id A x) := id <*> rec (hr, π) ; + wh_red_stack (?(tRefl A x) ,cons (eIdElim _ _ _ hr _) π) (tm_view1_id A x) := rec (hr, π) ; wh_red_stack (_ ,cons _ _) (tm_view1_id _ _) := undefined ; wh_red_stack (t ,nil) (tm_view1_type _) := ret t ; wh_red_stack (t ,cons s _) (tm_view1_type _) := undefined. @@ -631,12 +631,12 @@ Equations typing_wf_ty : typing_stmt wf_ty_state := | ty_view1_ty (eSort s) := success ; | ty_view1_ty (eProd A B) := rA ← rec (wf_ty_state;Γ;tt;A) ;; - id <*> rec (wf_ty_state;Γ,,A;tt;B) ; + rec (wf_ty_state;Γ,,A;tt;B) ; | ty_view1_ty (eNat) := success ; | ty_view1_ty (eEmpty) := success ; | ty_view1_ty (eSig A B) := rA ← rec (wf_ty_state;Γ;tt;A) ;; - id <*> rec (wf_ty_state;Γ,,A;tt;B) ; + rec (wf_ty_state;Γ,,A;tt;B) ; | ty_view1_ty (eId A x y) := rA ← rec (wf_ty_state;Γ;tt;A) ;; rec (check_state;Γ;A;x) ;;