VSU.v: removed some intermediate simplicifications in SC_tac as they …

…lead to nontermination in some examples. Variant with mk_funspecs_congr likewise fails on some examples that require additional change_compspecs applications to user-defined predicates. forward.v: added the two compspecs in questions in the warning message to make it more informative

floyd/VSU.v

@@ -880,6 +880,40 @@ Ltac HImports_tac' := clear; repeat apply Forall_cons; try apply Forall_nil;
                        fail "Imports disagree at identifier" i end).
 
 Ltac SC_tac :=
+ match goal with |- SC_test ?ids _ _ =>
+  let a := eval compute in ids in change ids with a
+ end;
+ simpl SC_test;
+ repeat (apply conj);
+ lazymatch goal with
+         | |- Funspecs_must_match ?i _ _ =>
+                 try solve [constructor; unfold abbreviate; 
+                 repeat f_equal
+                 (*occasionally leaves a subgoal, typically because a
+                   change_compspecs needs to be inserted that could not
+                    be identified automatically*)]
+         | |- Identifier_not_found ?i ?fds2 =>
+                 fail "identifer" i "not found in funspecs" fds2
+         | |- True => trivial
+          end.
+(*Alternatives:
+Ltac SC_tac1 :=
+ match goal with |- SC_test ?ids _ _ =>
+  let a := eval compute in ids in change ids with a
+ end;
+ simpl SC_test;
+ repeat (apply conj);
+ lazymatch goal with
+         | |- Funspecs_must_match ?i _ _ =>
+                 try solve [constructor; unfold abbreviate; 
+                 (*leads sometimes to nontermination: try simple apply eq_refl;*)
+                 repeat f_equal]
+         | |- Identifier_not_found ?i ?fds2 =>
+                 fail "identifer" i "not found in funspecs" fds2
+         | |- True => trivial
+          end.
+
+Ltac SC_tac2 :=
  match goal with |- SC_test ?ids _ _ =>
   let a := eval compute in ids in change ids with a
  end;
@@ -892,12 +926,13 @@ Ltac SC_tac :=
                  [ try reflexivity 
                  | try reflexivity 
                  | try reflexivity
-                 | try (apply eq_JMeq; trivial)
-                 | try (apply eq_JMeq; trivial)]
+                 | (*too aggressive here: try (apply eq_JMeq; trivial)*)
+                 | (*too aggressive here: try (apply eq_JMeq; trivial)*)]
          | |- Identifier_not_found ?i ?fds2 =>
                  fail "identifer" i "not found in funspecs" fds2
          | |- True => trivial
           end.
+*)
 
 Ltac HImports_tac := simpl;
   let i := fresh "i" in 

floyd/forward.v

@@ -712,9 +712,9 @@ a "versus" b ")"
  else fail
 end.
 
-Ltac change_compspecs_warning A := 
-     idtac "Remark: change_compspecs on user-defined mpred:" A
- "(to disable this message, Ltac change_compspecs_warning A ::= idtac".
+Ltac change_compspecs_warning A cs cs' := 
+     idtac "Remark: change_compspecs on user-defined mpred:" A cs cs'
+ "(to disable this message, Ltac change_compspecs_warning A cs cs' ::= idtac".
 
 Ltac change_compspecs' cs cs' :=
   lazymatch goal with
@@ -725,22 +725,22 @@ Ltac change_compspecs' cs cs' :=
   | |- _ => 
     match goal with 
   | |- context [?A cs'] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs') with (A cs)
   | |- context [?A cs' ?B] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B) with (A cs B)
   | |- context [?A cs' ?B ?C] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C) with (A cs B C)
   | |- context [?A cs' ?B ?C ?D] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D) with (A cs B C D)
   | |- context [?A cs' ?B ?C ?D ?E] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D E) with (A cs B C D E)
   | |- context [?A cs' ?B ?C ?D ?E ?F] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D E F) with (A cs B C D E F)
    end
  end.