Estou tentando provar um teorema de correção para inserção em uma fila de prioridades baseada em lista. Aqui estão a função de inserção, a propriedade indutiva e a prova com a qual estou trabalhando:
Fixpoint insert (x : nat) (l : list nat) : list nat :=
match l with
| [] => [x]
| h :: t => if x <=? h then x :: h :: t else h :: insert x t
end.
Inductive list_PQ_property : list nat -> Prop :=
| sorted_empty : list_PQ_property []
| sorted_one : forall x, list_PQ_property [x]
| sorted_add : forall x y l,
x <= y ->
list_PQ_property (y :: l) ->
list_PQ_property (x :: y :: l).
Theorem insert_correctness :
forall (pq : PQ) (x : el),
list_PQ_property pq ->
list_PQ_property (insert x pq).
Proof.
intros pq x H.
induction H as [ | y | a b l Hab IHl].
- simpl. apply sorted_one.
- simpl. destruct (x <=? y) eqn:E.
+ apply Nat.leb_le in E. apply sorted_add.
* apply E.
* apply sorted_one.
+ apply Nat.leb_gt in E.
apply Nat.lt_le_incl in E.
apply sorted_add.
* apply E.
* apply sorted_one.
- simpl. destruct (x <=? a) eqn:E.
+ apply Nat.leb_le in E.
apply sorted_add.
* apply E.
* apply sorted_add.
-- apply Hab.
-- apply IHl.
+ destruct (x <=? b) eqn:E'.
* apply Nat.leb_le in E'.
apply sorted_add.
apply Nat.lt_le_incl.
apply Nat.leb_gt in E. apply E.
apply sorted_add.
++ apply E'.
++ apply IHl.
* apply Nat.leb_gt in E'.
apply sorted_add.
-- apply Hab.
Admitted.
Quando comecei a prova, tudo foi simples até chegar ao terceiro caso. No início, fiquei preso no
apply sorted_add.
++ apply E'.
++ apply IHl.
em que meu objetivo era, b <= xmas minha hipótese para E' era, x <= baté que eu contornei as propriedades de transitividade aplicando um monte de funções Nat encontradas em Coq. Agora estou preso em onde minha hipótese IHIHl se parece com isso:
IHIHl : list_PQ_property (insert x (b :: l))
mas meu objetivo é este:
list_PQ_property (b :: insert x l).
Não tenho certeza de como consertar isso ou se estou provando isso corretamente.
Qualquer orientação será apreciada.
Para mais informações, meu objetivo completo até agora é o seguinte:
1 goal
x : el
a, b : nat
l : list nat
Hab : a <= b
IHl : list_PQ_property (b :: l)
IHIHl : list_PQ_property (insert x (b :: l))
E : (x <=? a) = false
E' : b < x
______________________________________(1/1)
list_PQ_property (b :: insert x l)
Tentei usar IHIHl, mas não adiantou. Estou um pouco perdido, pois acho que foi assim que construí minha prova.