Roland Coeurjoly Lechuga (Jun 13 2022 at 20:17): 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
Roland Coeurjoly Lechuga (Jun 15 2022 at 10:15):I think I am going to ask this in Stack exchange
Last updated: Oct 13 2024 at 01:02 UTC