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: Jun 25 2024 at 17:02 UTC