CODEWITHSUNDEEP
lambdacoqtheorylambda-calculuscoq-tactic
Vlad
Vlad

Reputation: 3

Theorem for lambda calculus

I have to solve this exercise:

Formulate and prove a confluence theorem for lambda calculus (ie, prove that if a λ-expression e reduces to both e1 and e2, then there exists e' such that e1 and e2 reduce to e').

and this is my approach to this :

Notation "'λ' x , t" := (t_abs x t) (at level 60).
Notation "t1 @ t2" := (t_app t1 t2) (at level 50, left associativity).
Fixpoint subst (t : Term) (x : string) (s : Term) : Term :=
  match t with
  | t_var y => if String.eqb x y then s else t
  | t_abs y t1 => if String.eqb x y then t_abs y t1 else t_abs y (subst t1 x s)
  | t_app t1 t2 => t_app (subst t1 x s) (subst t2 x s)
  end.

Inductive beta_reduction : Term → Term → Prop :=
| beta_step : forall x t1 t2,
    beta_reduction (t_abs x t1 @ t2) (subst t1 x t2)
| beta_left : forall t1 t2 t1',
    beta_reduction t1 t1' → beta_reduction (t_app t1 t2) (t_app t1' t2)
| beta_right : forall t1 t2 t2',
    beta_reduction t2 t2' → beta_reduction (t_app t1 t2) (t_app t1 t2').
Inductive beta_reduction_star : Term → Term → Prop :=
| beta_refl : forall t, beta_reduction_star t t
| beta_trans : forall t1 t2 t3,
    beta_reduction t1 t2 → beta_reduction_star t2 t3 → beta_reduction_star t1 t3.
Lemma confluence : forall t t1 t2,
  beta_reduction_star t t1 →
  beta_reduction_star t t2 →
  exists t', beta_reduction_star t1 t' ∧ beta_reduction_star t2 t'.
Proof.
  intros t t1 t2 H1 H2.
  induction H1 as [| t t0 t1 H Hstar IH].
  - (* cazul de bază: t1 = t *)
    exists t2.
    split.
    + exact H2.
    + apply beta_refl.
  - assert (beta_reduction_star t0 t2) as Hstep.
    {
      apply beta_trans with (t2 := t).
      - exact H. (* here is the problem *)
      - exact H2.
    }
    destruct (IH Hstep) as [t' [H3 H4]].
    exists t'.
    split.
    + apply beta_trans with (t2 := t0).
      * exact Hstar. (* t0 ->* t1 *)
      * exact H3.    (* t1 ->* t' *)
    + exact H4. (* t2 ->* t' *)
Qed.

the thing is I am getting this error:

In environment
t2, t, t0, t1 : Term
H : beta_reduction t t0
Hstar : beta_reduction_star t0 t1
H2 : beta_reduction_star t t2
IH : beta_reduction_star t0 t2 → ∃ t' : Term, beta_reduction_star t1 t' ∧ beta_reduction_star t2 t'
The term "H" has type "beta_reduction t t0" while it is expected to have type "beta_reduction t0 t".

i put a comment next to the broken line of code that produces the error.

  • exact H. (* here is the problem *)

Upvotes: 0

Views: 73

Answers (1)

Dominique Larchey-Wendling
Dominique Larchey-Wendling

Reputation: 201

Btw your code for substitution is not correct because it is not "capture avoiding" !!! May I suggest switching to the De Bruijn handling of binders?

Upvotes: 1

Related Questions