From 85296576dfa90a9f25f7d77ebe697ee23e5571c3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 23 Jan 2024 17:54:11 +0100 Subject: [PATCH] refactoring --- examples/stuck.v | 22 +++++++--------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/examples/stuck.v b/examples/stuck.v index f0ff441..08f2974 100644 --- a/examples/stuck.v +++ b/examples/stuck.v @@ -20,17 +20,17 @@ Set Universe Polymorphism. Local Open Scope int_scope. Local Open Scope Zmodp_scope. -Module Stuck. - Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp Param01_paths Param10_paths Radd Rzero. -Trocq Use Param44_list Param_cons Param_nil. +Trocq Use Rp Param01_paths Param10_paths Radd Rzero Param_cons Param_nil. + +Module Stuck. +Trocq Use Param44_list. Goal forall (l : list Zmodp), l = l. Fail trocq. Abort. @@ -39,19 +39,11 @@ End Stuck. Module Works. -Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). - -Axiom Rzero : Rp zerop zero. -Variable Radd : binop_param Rp Rp Rp addp add. -Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. - -Trocq Use Rp Param01_paths Param10_paths Radd Rzero. -Trocq Use Param2a4_list Param_cons Param_nil. - +Trocq Use Param2a4_list. Goal forall (l : list Zmodp), l = l. trocq. -Abort. +reflexivity. +Qed. End Works. -