So I'm at a subgoal
f initial_value a = initial_value
where the assumptions are the following
initial_value: state
l: list arg
a: arg
and the definition of arg
, state
and f
are the following
Parameter state : Type.
Parameter arg : Type.
Parameter f : state -> arg -> state.
I don't know if this can be proved but I think intuitively this makes sense because the types match
So I don't know what else I should do to prove this?
If I can evaluate the function then it would solve it to a degree but I don't think it's possible since it is a parameter and has not concrete definition
Parameter is like a variable but at the module level
for instance if you could prove it you could do this
Module Type T.
Parameter state : Type.
Parameter arg : Type.
Parameter f : state -> arg -> state.
End T.
Module F (X:T).
Import X.
Lemma the_thing initial_value a : f initial_value a = initial_value.
Proof. Admitted.
End F.
Module A.
Definition state := bool.
Definition arg := unit.
Definition f (x:bool) (_:unit) := true.
End A.
Module M := F A.
Definition wtf : true = false := M.the_thing false tt.
oh ok, yeah this makes sense, that is an illegal proof.
I was trying to prove a fold_left
statement and then try to prove the assert statement as a Lemma which lead me to the subgoal.
Theorem fold_invariant :
forall (P : state -> Prop)
(l : list arg)
(initial_value : state)
(Hind : forall x state, P state -> P (f state x))
(H0 : P initial_value),
P (fold_left f l initial_value).
intros.
generalize dependent initial_value.
induction l; simpl.
- auto.
- simpl in *.
intros.
apply IHl in H0.
assert (HH : fold_left f l initial_value = fold_left f l (f initial_value a)) by admit.
rewrite HH in H0.
assumption.
Admitted.
I don't know if this statement makes any sense
I was just confused and I thought at least I'm getting somewhere with this assertion
You were very close to the solution!
Theorem fold_invariant :
forall (P : state -> Prop)
(l : list arg)
(initial_value : state)
(Hind : forall x state, P state -> P (f state x))
(H0 : P initial_value),
P (fold_left f l initial_value).
Proof.
intros; generalize dependent initial_value.
induction l; simpl.
- auto.
- simpl in *.
intros; apply (IHl (f initial_value a)), Hind; assumption.
Qed.
Oh thanks! I didn't realize we can pass arguments to hypothesis, thanks for the help @Pierre Castéran :relieved:
Note that apply
is able to guess the right arguments of IHl
.
intros;apply IHl; auto. (* replaces the last line of the proof script *)
Even shorter: just auto
.
Last updated: Oct 13 2024 at 01:02 UTC