subexpr.v

Require Import Arith Lia List String.

Set Implicit Arguments.

Definition eq_dec (A : Type) :=
  forall (x : A),
    forall (y : A),
      {x = y} + {x <> y}.

Notation var := string.
Definition var_eq : eq_dec var := string_dec.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

Inductive subexpr : arith -> arith -> Prop :=
| subexpr_refl :
  forall e,
    subexpr e e
| subexpr_inl_plus :
  forall e1 e1' e2,
   subexpr e1' e1 ->
   subexpr e1' (Plus e1 e2)
| subexpr_inl_minus :
  forall e1 e1' e2,
    subexpr e1' e1 ->
    subexpr e1' (Minus e1 e2)
| subexpr_inl_times :
  forall e1 e1' e2,
    subexpr e1' e1 ->
    subexpr e1' (Times e1 e2)
| subexpr_inr_plus :
  forall e1 e2' e2,
    subexpr e2' e2 ->
    subexpr e2' (Plus e1 e2)
| subexpr_inr_minus :
  forall e1 e2' e2,
    subexpr e2' e2 ->
    subexpr e2' (Minus e1 e2)
| subexpr_inr_times :
  forall e1 e2' e2,
    subexpr e2' e2 ->
    subexpr e2' (Times e1 e2).
Local Hint Constructors subexpr : core.

Section subexpr_inversion.
  
Ltac subexpr_solve := intros; inversion H; subst; auto.
Lemma subexpr_const_inversion : 
 forall e n, subexpr e (Const n) -> (e = Const n).
Proof.
  subexpr_solve.
Qed.

Lemma subexpr_var_inversion : 
 forall e x, subexpr e (Var x) -> (e = Var x).
Proof.
  subexpr_solve.
Qed.

Lemma subexpr_plus_inversion : 
  forall e e1 e2, subexpr e (Plus e1 e2)
  -> (e = Plus e1 e2) \/ (subexpr e e1) \/ (subexpr e e2).
Proof.
  subexpr_solve.
Qed.

Lemma subexpr_minus_inversion : 
  forall e e1 e2, subexpr e (Minus e1 e2)
  -> (e = Minus e1 e2) \/ (subexpr e e1) \/ (subexpr e e2).
Proof.
  subexpr_solve.
Qed.

Lemma subexpr_times_inversion : 
  forall e e1 e2, subexpr e (Times e1 e2)
  -> (e = Times e1 e2) \/ (subexpr e e1) \/ (subexpr e e2).
Proof.
  subexpr_solve.
Qed.

End subexpr_inversion.

Section proper_subexpr.

Require Import Wellfounded.Well_Ordering.

Definition eq_dec_arith : eq_dec arith.
Proof.
  unfold eq_dec. decide equality.
  - apply Nat.eq_dec.
  - apply var_eq.
Qed.

Definition proper_subexpr e' e := (e' <> e) /\ subexpr e' e.

Lemma proper_subexpr_defn
  : forall e' e, subexpr e' e <-> proper_subexpr e' e \/ e' = e.
Proof.
  intros. split; intro.
  - destruct (eq_dec_arith e' e).
    + right. assumption
    + left.
    + left. constructor; assumption.
  - destruct H.
    + unfold proper_subexpr in H. destruct H; assumption.
    + rewrite H. constructor.
Qed.

Lemma proper_subexpr_well_founded : well_founded proper_subexpr.
Proof.
  intro e. induction e.
  - constructor. intros. inversion H. inversion H1. contradiction.
  - constructor. intros. inversion H. inversion H1. contradiction.
  - constructor. intros. inversion H.
    pose (subexpr_plus_inversion H1).
    destruct o; [|destruct H2].
    + contradiction.
    + rewrite (proper_subexpr_defn y e1) in H2.
      destruct H2.
      * apply IHe1. assumption.
      * congruence.
    + rewrite (proper_subexpr_defn y e2) in H2.
      destruct H2.
      * apply IHe2. assumption.
      * congruence.
  - constructor. intros. inversion H.
    pose (subexpr_minus_inversion H1).
    destruct o; [|destruct H2].
    + contradiction.
    + rewrite (proper_subexpr_defn y e1) in H2.
      destruct H2.
      * apply IHe1. assumption.
      * congruence.
    + rewrite (proper_subexpr_defn y e2) in H2.
      destruct H2.
      * apply IHe2. assumption.
      * congruence.
  - constructor. intros. inversion H.
    pose (subexpr_times_inversion H1).
    destruct o; [|destruct H2].
    + contradiction.
    + rewrite (proper_subexpr_defn y e1) in H2.
      destruct H2.
      * apply IHe1. assumption.
      * congruence.
    + rewrite (proper_subexpr_defn y e2) in H2.
      destruct H2.
      * apply IHe2. assumption.
      * congruence.
Qed.

Lemma well_founded_no_loops (A : Type) (R : A -> A -> Prop) (H : well_founded R)
  : forall x y, not (R x y /\ R y x).
Proof.
  intro x. specialize (H x). induction H.
  intros y H1. destruct H1.
  eapply H0.
  eassumption.
  split; eassumption.
Qed.

End proper_subexpr.

Theorem subexpr_anti_symmetry :
  forall e1 e2,
  subexpr e1 e2 ->
  subexpr e2 e1 ->
  e1 = e2.
Proof.
  intros. destruct (eq_dec_arith e1 e2); auto.
  assert (e2 <> e1) by (apply not_eq_sym; assumption).
  assert (proper_subexpr e1 e2) by (constructor; assumption).
  assert (proper_subexpr e2 e1) by (constructor; assumption).
  assert False.
  - eapply (well_founded_no_loops proper_subexpr_well_founded).
    split; eassumption.
  - contradiction.
Qed.