Stream: Coq users

Topic: Understanding &proving dependently typed Program obligation


view this post on Zulip Roland Coeurjoly Lechuga (Jun 13 2022 at 20:17):

I have written a dependently typed program, called generic_debugging_algorithm_dependently_typed2, with 4 obligations, of which I have proven 3.

This is the Program:

Program Fixpoint generic_debugging_algorithm_dependently_typed2 (n : {n: Node | is_debugging_tree n}) {measure (weight n)}: {m: Node | is_debugging_tree m /\ is_node_in_tree (content m) n} :=
  match children n with
    nil => n
  | head::tail => generic_debugging_algorithm_dependently_typed2 (get_debugging_tree_from_tree head)
  end.

This is the obligation that remains unproven.

  is_debugging_tree
    (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:=n)
                generic_debugging_algorithm_dependently_typed2
                Heq_anonymous))
          (generic_debugging_algorithm_dependently_typed2_obligation_3
             (n:=n)
             generic_debugging_algorithm_dependently_typed2
             Heq_anonymous))) /\
  is_node_in_tree
    (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:=n)
                generic_debugging_algorithm_dependently_typed2
                Heq_anonymous))
          (generic_debugging_algorithm_dependently_typed2_obligation_3
             (n:=n)
             generic_debugging_algorithm_dependently_typed2
             Heq_anonymous))).(content)
    (proj1_sig n)

To me, this seems to mean I have to prove that the Program returns a value that satisfies the output dependent type when the input node has children.

I think I have all the needed lemmas already proven. However, I donĀ“t understand why there are previous obligations in the goal term.

Moreover, I have discharged all obligations of another Program with a similar output dependent type, generic_debugging_algorithm_dependently_typed.

Program Fixpoint generic_debugging_algorithm_dependently_typed (n : {n: Node | is_debugging_tree n}) {measure (weight n)}: {m: Node | is_debugging_tree m /\ children m = nil} :=
  match children n with
    nil => n
  | head::tail => generic_debugging_algorithm_dependently_typed (get_debugging_tree_from_tree head)
  end.

I have tried to inspect the obligations of this generic_debugging_algorithm_dependently_typed to help with the second one, but I see no obligation for the output dependent type! I am very confused about this.

Since the code is too long and cannot paste here, you can find the code here

view this post on Zulip Roland Coeurjoly Lechuga (Jun 15 2022 at 10:15):

I think I am going to ask this in Stack exchange


Last updated: Jan 29 2023 at 01:02 UTC