Stream: Coq users

Topic: How to simplify obligation for Program Fixpoint

view this post on Zulip Roland Coeurjoly Lechuga (Jun 18 2022 at 17:14):

I have the following goal:

head.(content) =
  (proj1_sig
     (generic_debugging_algorithm_dependently_typed2
        (exist
           (fun n0 : Node => is_debugging_tree n0)
           (get_debugging_tree_from_tree head)
           (generic_debugging_algorithm_dependently_typed2_obligation_2
              (n:=exist
                    (fun n0 : Node =>
                     is_debugging_tree n0) n H)
              generic_debugging_algorithm_dependently_typed2
              Heq_anonymous))
        (generic_debugging_algorithm_dependently_typed2_obligation_3
           (n:=exist
                 (fun n0 : Node =>
                  is_debugging_tree n0) n H)
           generic_debugging_algorithm_dependently_typed2
           Heq_anonymous))).(content)

I am confused about the inclusion of obligations I have already proved like:

generic_debugging_algorithm_dependently_typed2_obligation_2
generic_debugging_algorithm_dependently_typed2_obligation_3

Is it possible to simplify this? I tried

simpl.
Tactics.program_simpl.
intuition.

but nothing worked.

view this post on Zulip Kenji Maillard (Jun 18 2022 at 17:39):

Did you conclude your previous obligations with Qed ? If that's the case you won't be able to unfold the content of these obligations (one possible fix might then be to replace Qed with Defined).

Last updated: Oct 13 2024 at 01:02 UTC