## Stream: Coq users

### Topic: Function evaluation to prove type equality

#### kumar (Jul 03 2022 at 19:10):

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

#### Gaëtan Gilbert (Jul 03 2022 at 19:31):

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.
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.
``````

#### kumar (Jul 03 2022 at 19:37):

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.
``````

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

#### Pierre Castéran (Jul 03 2022 at 19:48):

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.
``````

#### kumar (Jul 03 2022 at 22:27):

Oh thanks! I didn't realize we can pass arguments to hypothesis, thanks for the help @Pierre Castéran :relieved:

#### Pierre Castéran (Jul 04 2022 at 05:32):

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: Feb 04 2023 at 21:02 UTC