Stream: Coq users

Topic: Function evaluation to prove type equality


view this post on Zulip 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

view this post on Zulip 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.
  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.

view this post on Zulip 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.
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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Pierre Castéran (Jul 04 2022 at 05:32):

Note that applyis 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