text:
Create HintDb hdb.

Require Import Ring.
Require Import Morphisms.

Section Integers.
  Inductive PosZ : Set :=
  | pz_one : PosZ
  | pz_succ : PosZ -> PosZ.

  Fixpoint PosZadd (n m : PosZ) : PosZ :=
  match n with
  | pz_one => pz_succ m
  | pz_succ n' => pz_succ (PosZadd n' m)
  end.

  Fixpoint PosZmultiply (n m : PosZ) : PosZ :=
  match n with
  | pz_one => m
  | pz_succ n' => PosZadd (PosZmultiply n' m) m
  end.

  Inductive Nat : Set :=
  | nat_zero : Nat
  | nat_succ : Nat -> Nat.

  Fixpoint inject_PZ_Nat (n : PosZ) : Nat :=
  match n with
  | pz_one => nat_succ nat_zero
  | pz_succ n' => nat_succ (inject_PZ_Nat n')
  end.

  Coercion inject_PZ_Nat : PosZ >-> Nat.

  Lemma PosZ_not_Nat_zero : forall n : PosZ,
    inject_PZ_Nat n <> nat_zero.
  Proof.
    intros n H. induction n; discriminate.
  Qed.

  Inductive Int : Set :=
  | zero : Int
  | succ : Int -> Int
  | pred : Int -> Int.

  Fixpoint inject_Nat_Int (n : Nat) : Int :=
  match n with
  | nat_zero => zero
  | nat_succ n' => succ (inject_Nat_Int n')
  end.

  Coercion inject_Nat_Int : Nat >-> Int.

  Lemma PosZ_not_Int_zero : forall n : PosZ,
    inject_Nat_Int (inject_PZ_Nat n) <> nat_zero.
  Proof.
    intros n H. induction n; discriminate.
  Qed.

  Declare Scope Int_scope.
  Delimit Scope Int_scope with Int.
  Bind Scope Int_scope with Int.
  Open Scope Int_scope.
  Notation "1" := (pz_one) : Int_scope.
  Notation "0" := (nat_zero) : Int_scope.
  Notation "-1" := (pred zero) : Int_scope.

  Axiom pred_succ : forall (n : Int), pred (succ n) = n.

  Axiom succ_pred : forall (n : Int), succ (pred n) = n.

  Lemma equiv_succ :
    forall (n m : Int), n = m <-> succ n = succ m.
  Proof.
    split. intro.
    apply f_equal with (f:= fun t => succ t) in H.
    apply H.
    intro. apply f_equal with (f := fun t => pred t) in H.
    rewrite pred_succ in H.
    symmetry in H. rewrite pred_succ in H.
    symmetry in H. apply H.
  Qed.

  Lemma equiv_pred :
    forall (n m : Int), n = m <-> pred n = pred m.
  Proof.
    split. intro.
    apply f_equal with (f:= fun t => pred t) in H.
    apply H.
    intro. apply f_equal with (f := fun t => succ t) in H.
    rewrite succ_pred in H.
    symmetry in H. rewrite succ_pred in H.
    symmetry in H. apply H.
  Qed.

  Fixpoint Zadd (n m : Int) : Int :=
  match n with
  | zero => m
  | succ n' => succ (Zadd n' m)
  | pred n' => pred (Zadd n' m)
  end.

  Arguments Zadd _%Int _%Int.

  Infix "+" := Zadd (at level 50, left associativity) : Int_scope.

  Theorem PosZadd_Zadd_coincide : forall (a b : PosZ),
    inject_Nat_Int (inject_PZ_Nat (PosZadd a b)) = a + b.
  Proof.
    intros. induction a. trivial.
    simpl. rewrite IHa. reflexivity.
  Qed.

  Lemma add_zero_r : forall (n : Int), n + zero = n.
  Proof.
    intros. induction n.
    simpl. reflexivity.
    simpl. rewrite IHn. reflexivity.
    simpl. apply f_equal with (f := fun t => pred t). apply IHn.
  Qed.
  Hint Resolve add_zero_r : hdb.

  Lemma add_zero_l : forall (n : Int), zero + n = n.
  Proof.
    intros. simpl. reflexivity.
  Qed.
  Hint Resolve add_zero_l : hdb.

  Lemma add_zero_m : forall (n m : Int), n + zero + m = n + m.
  Proof.
    intros. rewrite add_zero_r. reflexivity.
  Qed.
  Hint Resolve add_zero_m : hdb.

  Lemma add_succ : forall (n m : Int), succ (n + m) = n + (succ m).
  Proof.
    intros. induction n.
    simpl. reflexivity.
    simpl. rewrite <- IHn. reflexivity.
    simpl. rewrite <- IHn.
    rewrite succ_pred. rewrite pred_succ. reflexivity.
  Qed.
  Hint Resolve add_succ : hdb.

  Lemma add_pred : forall (n m : Int), pred (n + m) = n + (pred m).
  Proof.
    intros. induction n.
    simpl. reflexivity.
    simpl. rewrite <- IHn.
    rewrite succ_pred. rewrite pred_succ. reflexivity.
    simpl. rewrite <- IHn. reflexivity.
  Qed.
  Hint Resolve add_pred : hdb.

  Theorem add_assoc :
    forall (i j k : Int), i + (j + k) = (i + j) + k.
  Proof.
    intros. induction i.
    simpl. reflexivity.
    simpl. rewrite <- IHi. reflexivity.
    simpl. rewrite <- IHi. reflexivity.
  Qed.
  Hint Resolve add_assoc : hdb.

  Theorem add_comm : forall (n m : Int), n + m = m + n.
  Proof.
    intros.
    induction n.
    simpl. symmetry. apply add_zero_r.
    simpl. rewrite IHn. apply add_succ.
    simpl. rewrite IHn. apply add_pred.
  Qed.
  Hint Resolve add_comm : hdb.

  Lemma add_one : forall (n : Int), succ n = n + 1.
  Proof.
    intro. rewrite add_comm. simpl. reflexivity.
  Qed.
  Hint Resolve add_one : hdb.

  Theorem add_closure : forall (n m : Int), exists (x : Int), n + m = x.
  Proof.
    intros. now exists (n + m).
  Qed.

  Lemma equiv_add :
    forall (i j k : Int), i = j <-> (i + k) = (j + k).
  Proof.
    split. intro.
    apply f_equal with (f := fun t => t + k). apply H.
    intro. induction k.
    repeat rewrite add_zero_r in H. apply H.
    repeat rewrite <- add_succ in H. apply equiv_succ in H.
    apply IHk. apply H.
    apply IHk. rewrite <- add_pred in H.
    symmetry. rewrite <- add_pred in H.
    apply f_equal with (f := fun t => succ t) in H.
    rewrite succ_pred in H.
    symmetry. rewrite succ_pred in H.
    apply H.
  Qed.
  Hint Resolve equiv_add : hdb.

  Lemma add_permute : forall (i j k : Int), i + j + k = j + k + i.
  Proof.
    intros.
    rewrite <- add_comm. rewrite add_assoc.
    symmetry. rewrite <- add_assoc. rewrite add_comm.
    reflexivity.
  Qed.
  Hint Resolve add_permute : hdb.

  Fixpoint Zopp (n : Int) : Int :=
  match n with
  | zero => zero
  | succ n' => pred (Zopp n')
  | pred n' => succ (Zopp n')
  end.

  Notation "- n" := (Zopp n) : Int_scope.

  Lemma opp_succ : forall (n : Int), - (succ n) = pred (- n).
  Proof.
    intros. induction n. all: simpl; reflexivity.
  Qed.
  Hint Resolve opp_succ : hdb.

  Lemma opp_pred : forall (n : Int), - (pred n) = succ (- n).
  Proof.
    intros. induction n. all: simpl; reflexivity.
  Qed.
  Hint Resolve opp_pred : hdb.

  Notation "n - m" := (Zadd n (- m)) : Int_scope.

  Lemma opp_opp : forall (n : Int), - (- n) = n.
  Proof.
    intro. induction n. all: simpl. reflexivity.
    all: rewrite IHn; reflexivity.
  Qed.
  Hint Resolve opp_opp : hdb.

  Lemma opp_one : - (1) = -1.
  Proof.
    trivial.
  Qed.
  Hint Resolve opp_one : hdb.

  Lemma add_negone : forall (n : Int), pred n = n - 1.
  Proof.
    intro. rewrite add_comm. simpl. reflexivity.
  Qed.
  Hint Resolve add_one : hdb.

  Theorem add_inv : forall (n : Int), n - n = zero.
  Proof.
    intros. induction n. simpl; reflexivity.
    simpl. rewrite <- add_pred, IHn. apply succ_pred.
    simpl. rewrite <- add_succ, IHn. apply pred_succ.
  Qed.
  Hint Resolve add_inv : hdb.

  Lemma opp_distr : forall (n m : Int), - (n + m) = (- n) + (- m).
  Proof.
    intros. induction m. repeat rewrite add_zero_r. reflexivity.
    all: simpl. rewrite <- opp_succ.
    induction n. all: simpl. reflexivity.

    symmetry; rewrite <- opp_succ. rewrite IHn. reflexivity.
    apply f_equal with (f := fun t => - t) in IHm as IH2.
    rewrite opp_opp in IH2. simpl in IH2.
    apply equiv_succ in IH2.
    rewrite IH2. rewrite opp_opp. reflexivity.

    symmetry; rewrite <- opp_succ. rewrite IHn. reflexivity.
    apply f_equal with (f := fun t => - t) in IHm as IH2.
    rewrite opp_opp in IH2. simpl in IH2.
    apply equiv_pred in IH2.
    rewrite IH2. rewrite opp_opp. reflexivity.

    rewrite <- add_succ. rewrite <- add_pred. rewrite opp_pred.
    apply -> equiv_succ. apply IHm.
  Qed.
  Hint Resolve opp_distr : hdb.

  Lemma swap_sides_eqn : forall i j k, i = j - k <-> i + k = j.
  Proof.
    split. intro. apply f_equal with (f := fun t => t + k) in H.
    rewrite <- add_assoc in H. rewrite H. rewrite add_comm, <- add_zero_r.
    symmetry. rewrite add_comm. apply equiv_add. rewrite add_comm, add_inv.
    reflexivity.
    intro. apply f_equal with (f := fun t => t - k) in H.
    rewrite <- add_assoc, add_inv, add_zero_r in H. assumption.
  Qed.

  Lemma eq_implies_add_inv : forall n m, n = m -> n - m = 0.
  Proof.
    intros. apply f_equal with (f := fun t => t - m) in H.
    rewrite add_inv in H. assumption.
  Qed.

  Lemma add_inv_implies_eq : forall n m, n - m = 0 -> n = m.
  Proof.
    intros. apply swap_sides_eqn in H.
    rewrite opp_opp in H. simpl in H.
    assumption.
  Qed.

  Inductive lte (n : Int) : Int -> Prop :=
  | lte_id : lte n n
  | lte_s : forall (m : Int), lte n m -> lte n (succ m).

  Definition lt (n m : Int) := lte (succ n) m.

  Notation gte a b := (lte b a) (only parsing).
  Notation gt a b := (lt b a) (only parsing).

  Infix "n <= m" := (lte n m) (at level 70, no associativity) : Int_scope.
  Infix "n < m" := (lt n m) (at level 70, no associativity) : Int_scope.
  Infix "n >= m" := (gte n m) (at level 70, no associativity) : Int_scope.
  Infix "n > m" := (gt n m) (at level 70, no associativity) : Int_scope.

  Theorem lte_not_1_0 : (lte 1 0 -> False).
  Proof.
    intro. inversion H.
  Qed.

  Lemma lte_invar_lr_add : forall (i j : Int),
    lte i j <-> (forall (n : Int), lte (i+n) (j+n)).
  Proof.
    split. intros. induction H. apply (lte_id (i + n)).
    rewrite add_one. rewrite <- add_permute. rewrite <- add_one.
    apply lte_s. replace (n + m) with (m + n). assumption.
    apply add_comm.

    intros. remember (H 0) as G. clear HeqG.
    repeat rewrite add_zero_r in G. assumption.
  Qed.

  Lemma lte_invar_lr_sub : forall (i j k : Int),
    lte (i+k) (j+k) -> lte i j.
  Proof.
    intros. apply lte_invar_lr_add with (n:= -k) in H.
    repeat rewrite <- add_assoc in H. rewrite add_inv in H.
    repeat rewrite add_zero_r in H. assumption.
  Qed.

  Lemma lt_not_id : forall n, lt n n -> False.
  Proof.
    intros. unfold lt in H. rewrite add_one in H.
    rewrite add_comm in H. replace (lte (1 + n) n) with (lte (1 + n) (0 + n)) in H.
    apply lte_invar_lr_sub in H. apply lte_not_1_0. assumption.
    trivial.
  Qed.

  Theorem lte_trans : forall i j k, lte i j -> lte j k -> lte i k.
  Proof.
    intros i j k H G.

    induction H. induction G. apply lte_id. apply lte_s. assumption.

    apply IHlte. apply lte_s in G.
    replace (succ k) with (k + 1) in G. rewrite add_one in G.
    apply lte_invar_lr_sub in G. assumption.
    rewrite <- add_one. reflexivity.
  Qed.

  Theorem lt_trans : forall i j k, lt i j -> lt j k -> lt i k.
  Proof.
    intros i j k H G. unfold lt. unfold lt in H, G.
    apply lte_s in G. rewrite add_one in G.
    replace (succ k) with (k + 1) in G.
    apply lte_invar_lr_sub in G.
    apply (lte_trans (succ i) j k H G).
    rewrite <- add_one. reflexivity.
  Qed.

  Theorem lte_min_or_more : forall i j, lte i j <-> i = j \/ lte (succ i) j.
  Proof.
    split. intro. induction H. left. reflexivity.
    destruct IHlte as [Ieq | Ilt].

    right. rewrite Ieq. apply lte_id.
    right. apply lte_s in Ilt. assumption.

    intro. destruct H as [Ieq | Ilt]. rewrite Ieq. apply lte_id.

    apply lte_s in Ilt.
    rewrite add_one in Ilt. replace (succ j) with (j + 1) in Ilt.
    apply lte_invar_lr_sub in Ilt. assumption.

    rewrite <- add_one. reflexivity.
  Qed.

  Theorem lte_max_or_less : forall i j, lte i j <-> i = j \/ lte i (pred j).
  Proof.
    split. intro. induction H. left. reflexivity.
    destruct IHlte as [Ieq | Ilt].

    right. rewrite Ieq, pred_succ. apply lte_id.
    right. apply lte_s in Ilt. rewrite succ_pred in Ilt.
    rewrite pred_succ. assumption.

    intro. destruct H as [Ieq | Ilt]. rewrite Ieq. apply lte_id.

    apply lte_s in Ilt.
    rewrite succ_pred in Ilt. assumption.
  Qed.

  Theorem lt_not_eq : forall i j, lt i j -> i <> j.
  Proof.
    intros. intro. induction i. induction j. unfold lt in H.

    apply lte_not_1_0. assumption.
    all: rewrite H0 in H; apply lt_not_id in H; assumption.
  Qed.

  Theorem lte_definite : forall i j, lte i j -> lte j i -> i = j.
  Proof.
    intros i j lte_ij lte_ji.

    apply lte_min_or_more in lte_ij. apply lte_min_or_more in lte_ji.
    destruct lte_ij as [eqij | ltij]. destruct lte_ji as [eqji | ltji].

    assumption. assumption.
    destruct lte_ji as [eqji | ltji].

    symmetry in eqji. assumption.
    set (H := lt_trans i j i ltij ltji).
    apply lt_not_id in H. contradiction.
  Qed.

  Lemma lte_opp : forall (a b : Int), lte a b -> lte (- b) (- a).
  Proof.
    intros. induction H. apply (lte_id (- a)).
    rewrite opp_succ.
    set (G := lte_id (pred (- m))).
    apply lte_s in G. rewrite succ_pred in G.
    apply (lte_trans (pred (-m)) (-m) (-a) G IHlte).
  Qed.

  Definition positive (n : Int) := lt zero n.
  Definition negative (n : Int) := lt n zero.

  Inductive positive' : Int -> Prop :=
  | pos_one : positive' 1
  | pos_s : forall (m : Int), positive' m -> positive' (m + 1).

  Inductive negative' : Int -> Prop :=
  | neg_one : negative' -1
  | neg_p : forall (m : Int), negative' m -> negative' (m - 1).

  Definition Sign (n : Int) := n = 0 \/ positive n \/ negative n.

  Definition positive_one : positive 1.
  Proof.
    apply (lte_id 1).
  Qed.

  Definition negative_one : negative -1.
  Proof.
    unfold negative, lt. rewrite succ_pred. apply (lte_id 0).
  Qed.

  Theorem int_sign : forall n, Sign n.
  Proof.
    intro. unfold Sign.
    unfold positive, negative, lt. simpl.
    induction n.
    left. reflexivity.

    all: destruct IHn as [Cz | [Cp | Cn]].

    right. left. rewrite Cz. apply (lte_id 1).
    right. left. apply lte_s. assumption.
    destruct Cn.
    left. reflexivity.
    right. right.
    rewrite (add_one (succ n)). rewrite (add_one m).
    apply lte_invar_lr_add with (n := 1). assumption.

    right. right. rewrite succ_pred, Cz. apply (lte_id 0).
    destruct Cp.
    left. rewrite pred_succ. reflexivity.
    right. left. rewrite pred_succ. assumption.
    right. right. rewrite succ_pred.
    apply lte_s in Cn.
    rewrite (add_one zero) in Cn. rewrite add_one in Cn.
    apply lte_invar_lr_sub with (k := 1) in Cn.
    assumption.
  Qed.

  Ltac destruct_sign n :=
    let Cs := fresh "Csign" in idtac;
    let Cz := fresh "Cz" in idtac;
    let Cp := fresh "Cp" in idtac;
    let Cn := fresh "Cn" in idtac;
    set (Cs := int_sign n);
    destruct Cs as [Cz | [Cp | Cn]];
    try rewrite Cz.

  Lemma positive_positive'_coincide : forall (n : Int),
    positive n <-> positive' n.
  Proof.
    split. intro. induction n.
    unfold positive, lt in H.
    apply lte_not_1_0 in H. contradiction.

    inversion H. apply pos_one. rewrite add_one. apply pos_s.
    apply IHn. assumption.

    induction H. apply pos_one. rewrite add_one. apply pos_s.
    assumption.

    intro. induction H. apply (lte_id 1).
    unfold positive. rewrite <- add_one. apply lte_s.
    assumption.
  Qed.

  Lemma negative_negative'_coincide : forall (n : Int),
    negative n <-> negative' n.
  Proof.
    split. intro. inversion H.
    intro. induction H.

    unfold negative. unfold lt. rewrite succ_pred.
    apply (lte_id 0).

    rewrite <- add_negone. unfold negative, lt. rewrite succ_pred.
    unfold negative, lt in IHnegative'.
    set (G := lte_id m). apply lte_s in G.
    apply (lte_trans m (succ m) 0 G IHnegative').
  Qed.

  Lemma lte_invar_r_add : forall (i j : Int),
    lte i j -> forall (n : Int), (n = 0 \/ positive n) -> lte i (j+n).
  Proof.
    intros. destruct H0 as [C0 | CP].
    rewrite C0, add_zero_r. assumption.
    apply positive_positive'_coincide in CP.
    induction CP. rewrite <- add_one. apply lte_s. assumption.
    rewrite add_assoc. rewrite <- add_one. apply lte_s.
    assumption.
  Qed.

  Lemma pos_sum : forall (n m : Int), positive n -> positive m -> positive (n + m).
  Proof.
    intros n m H G.
    apply positive_positive'_coincide in H, G.
    apply positive_positive'_coincide.

    induction G. apply pos_s. assumption.
    rewrite add_assoc. apply pos_s. assumption.
  Qed.

  Lemma neg_sum : forall (n m : Int), negative n -> negative m -> negative (n + m).
  Proof.
    intros n m H G.
    apply negative_negative'_coincide in H, G.
    apply negative_negative'_coincide.

    induction G. apply neg_p. assumption.
    rewrite add_assoc. apply neg_p. assumption.
  Qed.

  Theorem zero_signless : ((positive 0 -> False) /\ (negative 0 -> False))
    /\ ((positive' 0 -> False) /\ (negative' 0 -> False)).
  Proof.
    split.
    split; intro; apply lt_not_eq in H; contradiction.
    split; intro;
    apply positive_positive'_coincide in H ||
      apply negative_negative'_coincide in H;
    apply lt_not_eq in H; contradiction.
  Qed.

  Fixpoint abs (n : Int) :=
  match n with
  | zero => zero
  | succ n' => abs n' + 1
  | pred n' => abs n' + 1
  end.

  Lemma abs_pos : forall (n : Int), (n = 0) \/ positive (abs n).
  Proof.
    intros. induction n. left. reflexivity.

    all: destruct IHn; right; try rewrite H; simpl; try apply (lte_id 1).
    all: rewrite <- add_one; apply lte_s; assumption.
  Qed.

  Lemma abs_opp : forall (n : Int), abs (- n) = abs n.
  Proof.
    intro. induction n. trivial.
    all: rewrite opp_succ || rewrite opp_pred; simpl; rewrite IHn; reflexivity.
  Qed.

  Lemma pos_equiv_abs : forall (n : Int), positive n -> abs n = n.
  Proof.
    intros. induction H. simpl. reflexivity.
    simpl. rewrite <- add_one, IHlte. reflexivity.
  Qed.

  Lemma neg_equiv_abs : forall (n : Int), negative n -> abs n = - n.
  Proof.
    intros. inversion H.
  Qed.

  Lemma abs_pos_neg : forall (n : Int), abs n = n \/ abs n = - n.
  Proof.
    intros. destruct_sign n. left. simpl. reflexivity.
    left. apply (pos_equiv_abs n Cp).
    right. apply (neg_equiv_abs n Cn).
  Qed.

  Lemma abs_sum_ineq : forall (i j : Int), lte (abs (i + j)) (abs i + abs j).
  Proof.
    intros.

    induction j. simpl. repeat rewrite add_zero_r. apply lte_id.

    all: simpl; rewrite <- add_pred || rewrite <- add_succ; simpl;
    rewrite add_assoc; apply -> lte_invar_lr_add; assumption.
  Qed.

  Theorem abs_zero : forall n, abs n = 0 <-> n = 0.
  Proof.
    split.

    intro. set (G := abs_pos n). destruct G as [C0 | CG0].
    assumption.
    rewrite H in CG0. apply (lt_not_id 0) in CG0. contradiction.

    intro. rewrite H. trivial.
  Qed.

  Theorem triangle_ineq : forall (i j k : Int),
    lte (abs (i - k)) (abs (i - j) + abs (j - k)).
  Proof.
    intros. induction j. simpl. rewrite add_zero_r, abs_opp.
    induction k. simpl. repeat rewrite add_zero_r. apply (lte_id (abs i)).

    rewrite opp_succ. rewrite <- add_pred. simpl. rewrite add_assoc.
    apply -> lte_invar_lr_add. assumption.

    rewrite opp_pred. rewrite <- add_succ. simpl. rewrite add_assoc.
    apply -> lte_invar_lr_add. assumption.

    simpl. rewrite <- add_pred. simpl.
    rewrite add_assoc, <- add_one, <- add_permute, <- add_one.
    apply lte_s, lte_s.
    replace (abs (j - k) + abs (i - j)) with (abs (i - j) + abs (j - k)).
    assumption. rewrite add_comm. reflexivity.

    simpl. rewrite <- add_succ. simpl.
    rewrite add_assoc, <- add_one, <- add_permute, <- add_one.
    apply lte_s, lte_s.
    replace (abs (j - k) + abs (i - j)) with (abs (i - j) + abs (j - k)).
    assumption. rewrite add_comm. reflexivity.

  Qed.

  Fixpoint Zmultiply (n m : Int) : Int :=
  match n with
  | zero => zero
  | succ n' => (Zmultiply n' m) + m
  | pred n' => (Zmultiply n' m) - m
  end.

  Infix "*" := Zmultiply (at level 40, left associativity) : Int_scope.

  Theorem PosZmultiply_Zmultiply_coincide : forall (a b : PosZ),
    inject_Nat_Int (inject_PZ_Nat (PosZmultiply a b)) = a * b.
  Proof.
    intros. simpl. induction a.
    trivial.
    simpl. rewrite PosZadd_Zadd_coincide, IHa. reflexivity.
  Qed.

  Lemma multiply_zero : forall (n : Int), n * zero = zero.
  Proof.
    intro. induction n.
    simpl. reflexivity.
    all: simpl; rewrite add_zero_r; apply IHn.
  Qed.

  Lemma multiply_id_r : forall (n : Int), n * 1 = n.
  Proof.
    intro. simpl. induction n. trivial.
    all: simpl; rewrite IHn;
    rewrite <- add_succ || rewrite <- add_pred;
    rewrite add_zero_r; reflexivity.
  Qed.

  Lemma multiply_succ : forall (n m : Int), n * (succ m) = n * m + n.
  Proof.
    intros. induction n.
    simpl. reflexivity.
    simpl. rewrite IHn. rewrite add_permute, <- add_succ.
    symmetry. rewrite add_permute, <- add_succ.
    apply equiv_add. apply -> equiv_succ. apply add_comm.

    simpl. rewrite IHn. rewrite add_permute, <- add_pred.
    symmetry. rewrite add_permute, <- add_pred.
    apply equiv_add. apply -> equiv_pred. apply add_comm.
  Qed.

  Lemma multiply_pred : forall (n m : Int), n * (pred m) = n * m - n.
  Proof.
    intros. induction n.
    simpl. reflexivity.
    simpl. rewrite IHn. rewrite add_permute, <- add_pred.
    symmetry. rewrite add_permute, <- add_pred.
    apply equiv_add. apply -> equiv_pred. apply add_comm.

    simpl. rewrite IHn. rewrite add_permute, <- add_succ.
    symmetry. rewrite add_permute, <- add_succ.
    apply equiv_add. apply -> equiv_succ. apply add_comm.
  Qed.

  Lemma multiply_distr : forall (i j k : Int), i * (j + k) = i*j + i*k.
  Proof.
    intros. induction i.
    simpl. reflexivity.
    simpl. rewrite IHi. repeat rewrite add_assoc.
    apply equiv_add. rewrite <- add_permute.
    apply equiv_add. apply add_comm.
    simpl. rewrite opp_distr.
    replace (i * j - j + (i * k - k)) with (i * j + i * k + (- j - k)).
    apply equiv_add. apply IHi.
    rewrite add_permute. symmetry. rewrite add_permute.
    repeat rewrite add_assoc.
    repeat (apply equiv_add || apply add_comm).
  Qed.

  Lemma multiply_opp_r : forall (n m : Int), n * (- m) = - (n * m).
  Proof.
    intros. induction m.
    simpl. rewrite multiply_zero. trivial.
    all: simpl; rewrite multiply_succ, multiply_pred, opp_distr, IHm;
         try rewrite opp_opp; reflexivity.
  Qed.

  Lemma multiply_opp_l : forall (n m : Int), (- n) * m = - (n * m).
  Proof.
    intros. induction m.
    simpl. repeat rewrite multiply_zero. trivial.
    rewrite multiply_succ, multiply_succ, opp_distr, IHm. reflexivity.
    rewrite multiply_pred, multiply_pred, opp_distr, IHm. reflexivity.
  Qed.

  Lemma multiply_distr_sub : forall i j k, i * (j - k) = i * j - i * k.
  Proof.
    intros. rewrite multiply_distr, multiply_opp_r. reflexivity.
  Qed.

  Theorem multiply_comm : forall (n m : Int), n * m = m * n.
  Proof.
    intros. induction m.
    rewrite multiply_zero. simpl. reflexivity.
    rewrite multiply_succ. simpl. rewrite IHm. reflexivity.
    simpl. replace (pred m) with (pred (m + 0)).
    rewrite add_pred. rewrite multiply_distr. simpl.
    rewrite <- opp_one, multiply_opp_r, multiply_id_r, IHm. reflexivity.
    rewrite add_zero_r. reflexivity.
  Qed.

  Theorem multiply_assoc :
    forall (i j k : Int), i * (j * k) = (i * j) * k.
  Proof.
    intros. induction i. simpl. reflexivity.

    simpl. symmetry. rewrite multiply_comm.
    rewrite multiply_distr. rewrite multiply_comm.
    rewrite add_comm. symmetry. rewrite add_comm.
    rewrite IHi. apply equiv_add, multiply_comm.

    simpl. symmetry. rewrite multiply_comm, multiply_distr, multiply_opp_r.
    replace (k * j) with (j * k).
    apply equiv_add. rewrite multiply_comm.
    symmetry. apply IHi. apply multiply_comm.
  Qed.

  Theorem multiply_closure : forall (n m : Int), exists x, x = n * m.
  Proof.
    intros. now exists (n * m).
  Qed.

  Lemma multiply_permute : forall (i j k : Int), i * j * k = j * k * i.
  Proof.
    intros. symmetry. rewrite multiply_comm.
    apply multiply_assoc.
  Qed.

  Lemma Int_ring_theory : ring_theory zero (succ zero) Zadd Zmultiply (fun a b => a - b) Zopp eq.
  Proof.
    constructor. all: intros.
    rewrite add_comm, add_zero_r. reflexivity.
    apply add_comm.
    apply add_assoc.
    rewrite multiply_comm, multiply_id_r. reflexivity.
    apply multiply_comm.
    apply multiply_assoc.
    rewrite multiply_comm, multiply_distr, multiply_comm, add_comm, multiply_comm, add_comm. reflexivity.
    reflexivity.
    apply add_inv.
  Qed.

  Add Ring ZRing : Int_ring_theory.

  Lemma pos_multiply : forall (n m : Int), positive n -> positive m -> positive (n * m).
  Proof.
    intros n m H G. induction H. simpl. assumption.
    simpl. apply pos_sum. all: assumption.
  Qed.

  (*Theorem neg_neg_pos : forall n, negative (- n) -> positive n.
  Proof.
    intros k H.

    induction k. simpl in H.
    apply zero_signless in H; contradiction.
    rewrite add_one.
    unfold positive, lt. rewrite add_one, add_assoc.
    apply -> lte_invar_lr_add. rewrite add_zero_r.

    unfold positive, negative, lt in H, IHk.
    rewrite opp_succ, succ_pred in H.
    apply lte_invar_lr_add with (n:=k) in H.
    rewrite add_comm, add_inv in H. simpl in H. assumption.

    unfold positive, negative, lt in H, IHk.
    rewrite add_negone.
    unfold positive, lt.
    rewrite opp_pred, add_one, add_one in H.
    replace (lte (- k + 1 + 1) 0) with (lte (- k + 1 + 1) (-1 + 1)) in H.
    apply lte_invar_lr_sub in H. rewrite add_comm in H.
    apply lte_invar_lr_add with (n := k) in H.
    replace (1 - k + k) with 1 in H. replace (-1 + k) with (k - 1) in H.
    assumption. rewrite add_comm. reflexivity.
    symmetry. rewrite <- add_zero_r. symmetry. rewrite add_comm, add_permute.
    apply equiv_add. rewrite add_comm, add_inv. reflexivity.
    replace (-1 + 1) with 0. reflexivity.
    rewrite add_comm, add_inv. reflexivity.
  Qed.*)

  Theorem neg_neg_pos : forall n, negative (- n) -> positive n.
  Proof.
    intros. unfold negative, lt in H. unfold positive, lt.
    rewrite <- opp_pred in H.
    apply lte_opp in H.
    simpl in H. rewrite opp_opp in H.
    rewrite add_negone in H.
    apply lte_invar_lr_add with (n := 1) in H.
    rewrite opp_one, <- (add_assoc n -1 1), add_inv, add_zero_r in H.
    simpl in H. assumption.
  Qed.

  Theorem pos_neg_neg : forall n, positive n -> negative (- n).
  Proof.
    intros. unfold positive, lt in H. unfold negative, lt.
    rewrite <- opp_pred.
    apply (lte_opp zero (pred n)).
    replace (succ zero) with (0 + 1) in H by trivial.
    replace n with (n - 1 + 1) in H by ring.
    apply (lte_invar_lr_sub) in H.
    replace (n - 1) with (pred n) in H by (rewrite add_negone; reflexivity).
    assumption.
  Qed.

  Theorem positive_and_negative : forall (n : Int),
    positive n -> negative n -> False.
  Proof.
    intros n Hp Hn. apply pos_neg_neg in Hp.
    set (Hcon := neg_sum n (- n) Hn Hp).
    rewrite add_inv in Hcon. apply zero_signless in Hcon.
    contradiction.
  Qed.

  Theorem lte_add_pos_r : forall n m, positive m -> lt n (n + m).
  Proof.
    intros. induction n. assumption. simpl.
    replace (succ n) with (n + 1) by (rewrite <- add_one; reflexivity).
    replace (succ (n + m)) with (n + m + 1) by (rewrite <- add_one; reflexivity).
    unfold lt. replace (succ (n + 1)) with ((succ n) + 1) by trivial.
    apply lte_invar_lr_add with (n := 1). assumption.

    unfold lt. rewrite succ_pred. simpl.
    apply lte_invar_lr_sub with (k := 1).
    replace (n + 1) with (succ n) by (rewrite add_one; reflexivity).
    simpl. rewrite <- (add_succ (n + m)), pred_succ, add_zero_r.
    assumption.
  Qed.

  Theorem lte_add_neg_l : forall n m, negative m -> lt (n + m) n.
  Proof.
    intros. induction n. assumption. simpl.
    replace (succ n) with (n + 1) by (rewrite <- add_one; reflexivity).
    replace (succ (n + m)) with (n + m + 1) by (rewrite <- add_one; reflexivity).
    unfold lt. replace (succ (n + m + 1)) with (succ (n + m) + 1) by trivial.
    apply lte_invar_lr_add with (n := 1). assumption.

    unfold lt. simpl. rewrite succ_pred.
    apply lte_invar_lr_sub with (k := 1).
    replace (n + m + 1) with (succ (n + m)) by (rewrite add_one; reflexivity).
    replace (pred n + 1) with (n) by
      (rewrite <- add_one, succ_pred; reflexivity).
    assumption.
  Qed.

  Theorem abs_pos_sum : forall n m,
    positive n -> positive m -> abs (n + m) = abs n + abs m.
  Proof.
    intros n m H G.

    induction G. rewrite <- add_one. trivial.
    inversion H. simpl. symmetry. rewrite add_one. reflexivity.

    rewrite H1. rewrite <- add_succ. simpl.
    rewrite add_assoc. rewrite IHG. reflexivity.
  Qed.

  Theorem abs_neg_sum : forall n m,
    negative n -> negative m -> abs (n + m) = abs n + abs m.
  Proof.
    intros n m H G. rewrite <- opp_opp in H, G.
    apply neg_neg_pos in H, G.
    rewrite <- abs_opp.
    replace (abs n) with (abs (- n)) by (rewrite abs_opp; trivial).
    replace (abs m) with (abs (- m)) by (rewrite abs_opp; trivial).
    rewrite opp_distr.
    apply abs_pos_sum. all: assumption.
  Qed.

  Lemma pos_pos_product : forall (n m : Int),
    positive n -> positive m -> positive (n * m).
  Proof.
    intros n m H G.

    induction H. simpl. assumption.
    simpl. apply pos_sum. all: assumption.
  Qed.

  Lemma pos_neg_product : forall (n m : Int),
    positive n -> negative m -> negative (n * m).
  Proof.
    intros n m H G.

    inversion H. simpl. assumption.
    inversion G.
  Qed.

  Lemma neg_pos_product : forall (n m : Int),
    negative n -> positive m -> negative (n * m).
  Proof.
    intros n m H G.
    rewrite multiply_comm. apply (pos_neg_product m n G H).
  Qed.

  Lemma neg_neg_product : forall (n m : Int),
    negative n -> negative m -> positive (n * m).
  Proof.
    intros n m H G. inversion H.
  Qed.

  Lemma pos_product_sign : forall (n m : Int),
    positive (n * m) ->
      (positive n /\ positive m) \/ (negative n /\ negative m).
  Proof.
    intros n m H. destruct_sign n.
    rewrite Cz in H. simpl in H.
    apply zero_signless in H. contradiction.

    destruct_sign m.
    rewrite Cz in H. rewrite multiply_zero in H.
    apply zero_signless in H. contradiction.

    left. split; assumption.

    exfalso.
    set (Hcon := pos_neg_product n m Cp Cn).
    apply (positive_and_negative (n * m) H Hcon).

    destruct_sign m.
    rewrite Cz in H. rewrite multiply_zero in H.
    apply zero_signless in H. contradiction.

    exfalso.
    set (Hcon := neg_pos_product n m Cn Cp).
    apply (positive_and_negative (n * m) H Hcon).

    right. split; assumption.
  Qed.

  Lemma pos_product_pos : forall (n m : Int),
    positive n -> positive (n * m) -> positive m.
  Proof.
    intros n m H G. apply pos_product_sign in G.
    destruct G as [[Hnp Hmp] | [Hnn Hnm]].
    assumption.
    exfalso. apply (positive_and_negative n H Hnn).
  Qed.

  Lemma lazy_positive_to_lte : forall n, positive n -> lte 0 n.
  Proof.
    intros. unfold positive, lt in H.
    apply lte_s in H.
    rewrite add_one, (add_one n) in H.
    apply lte_invar_lr_sub in H.
    assumption.
  Qed.

  Lemma lazy_negative_to_lte : forall n, negative n -> lte n 0.
  Proof.
    intros. rewrite <- opp_opp in H.
    apply neg_neg_pos, lazy_positive_to_lte, lte_opp in H.
    ring_simplify in H. assumption.
  Qed.

  Lemma lte_abs : forall (n m : Int),
    positive m -> (lte (abs n) m <-> lte (- m) n /\ lte n m).
  Proof.
    split. intros.
    destruct_sign n.

    rewrite Cz in H0. simpl in H0.
    apply lte_opp in H0 as H2. simpl in H2.
    split; assumption.

    rewrite -> (pos_equiv_abs n Cp) in H0.
    apply pos_neg_neg in H.
    apply lazy_positive_to_lte in Cp.
    apply lazy_negative_to_lte in H.
    apply (lte_trans (- m) 0 n H) in Cp.
    split; assumption.

    rewrite -> (neg_equiv_abs n Cn) in H0.
    apply lte_opp in H0. ring_simplify in H0.
    apply lazy_positive_to_lte in H.
    apply lazy_negative_to_lte in Cn.
    apply (lte_trans n 0 m Cn) in H.
    split;assumption.

    intro. destruct H0.
    destruct (abs_pos_neg n).

    rewrite H2; assumption.
    rewrite H2. apply lte_opp in H0.
    ring_simplify in H0. assumption.
  Qed.

  Lemma abs_product_eq : forall (n m : Int),
    abs (n * m) = abs n * abs m.
  Proof.
    intros.

    destruct_sign n.
    simpl. reflexivity.
    all: destruct_sign m.

    simpl. repeat rewrite multiply_zero. simpl. reflexivity.

    set (H := pos_pos_product n m Cp Cp0).
    rewrite (pos_equiv_abs n Cp).
    rewrite (pos_equiv_abs m Cp0).
    rewrite (pos_equiv_abs (n * m) H).
    reflexivity.

    set (H := pos_neg_product n m Cp Cn).
    rewrite (pos_equiv_abs n Cp).
    rewrite (neg_equiv_abs m Cn).
    rewrite (neg_equiv_abs (n * m) H).
    rewrite multiply_opp_r. reflexivity.

    simpl. repeat rewrite multiply_zero. simpl. reflexivity.

    set (H := pos_neg_product m n Cp Cn). rewrite multiply_comm in H.
    rewrite (neg_equiv_abs n Cn).
    rewrite (pos_equiv_abs m Cp).
    rewrite (neg_equiv_abs (n * m) H).
    simpl. rewrite multiply_opp_l. reflexivity.

    set (H := neg_neg_product n m Cn Cn0).
    rewrite (neg_equiv_abs n Cn).
    rewrite (neg_equiv_abs m Cn0).
    rewrite (pos_equiv_abs (n * m) H).
    rewrite multiply_opp_r, multiply_opp_l, opp_opp. reflexivity.
  Qed.

  Lemma lte_invar_r_mul : forall (i j : Int),
    (j = 0 \/ positive j) -> lte i j ->
    forall (n : Int), positive n -> lte i (j * n).
  Proof.
    intros. induction H1.
    rewrite multiply_id_r. assumption.
    rewrite multiply_succ. apply lte_invar_r_add.
    all: assumption.
  Qed.

  Lemma abs_product_lte : forall (n m : Int),
    m <> 0 -> lte (abs n) (abs (n * m)).
  Proof.
    intros.
    rewrite abs_product_eq.
    set (Gn := abs_pos n). set (Gm := abs_pos m).
    destruct Gm. contradiction.

    apply lte_invar_r_mul.

    destruct Gn.
    left. apply abs_zero. assumption.
    right. assumption.
    apply (lte_id (abs n)). assumption.
  Qed.

  Lemma zero_implies_product_zero : forall (n m : Int),
    (n = 0) \/ (m = 0) -> n * m = 0.
  Proof.
    intros. destruct H as [H | G]. rewrite H. trivial.
    rewrite G, multiply_zero. reflexivity.
  Qed.

  Lemma product_zero_implies_zero : forall (n m : Int),
    n * m = 0 -> (n = 0) \/ (m = 0).
  Proof.
    intros.
    destruct_sign n. left. reflexivity.
    destruct_sign m. right. reflexivity.

    set (G := pos_pos_product n m Cp Cp0).
    rewrite H in G. apply zero_signless in G. contradiction.

    set (G := pos_neg_product n m Cp Cn).
    rewrite H in G. apply zero_signless in G. contradiction.

    destruct_sign m. right. reflexivity.

    set (G := neg_pos_product n m Cn Cp).
    rewrite H in G. apply zero_signless in G. contradiction.

    set (G := neg_neg_product n m Cn Cn0).
    rewrite H in G. apply zero_signless in G. contradiction.
  Qed.

  Lemma pos_neg_one_implies_product_one : forall (n m : Int),
    ((n = 1) /\ (m = 1)) \/ ((n = -1) /\ (m = -1)) -> n * m = 1.
  Proof.
    intros. destruct H; destruct H as [H G]; rewrite H, G; trivial.
  Qed.

  Theorem product_one_implies_pos_neg_one : forall (n m : Int),
    n * m = 1 -> ((n = 1) /\ (m = 1)) \/ ((n = -1) /\ (m = -1)).
  Proof.
    intros. apply f_equal with (f := fun t => abs t) in H as Habs.
    simpl in Habs.

    assert (m <> 0). intro. rewrite H0 in H.
    rewrite multiply_zero in H. discriminate.

    set (G := abs_product_lte n m H0).
    rewrite H in G. simpl in G.
    apply (lte_abs n 1 (lte_id 1)) in G. destruct G as [n_min n_max].

    assert (n <> 0).
    intro. rewrite H1 in H. simpl in H1. discriminate.

    set (G := abs_product_lte m n H1).
    rewrite multiply_comm, H in G. simpl in G.
    apply (lte_abs m 1 (lte_id 1)) in G. destruct G as [m_min m_max].

    apply lte_max_or_less in m_max.
    destruct m_max as [Cm1 | m_max].
    rewrite Cm1 in H. rewrite multiply_id_r in H.
    left. split; assumption.

    apply lte_min_or_more in m_min.
    destruct m_min as [Cmn1 | m_min].
    rewrite <- Cmn1 in H. rewrite multiply_opp_r, multiply_id_r in H.
    apply f_equal with (f := fun t => - t) in H.
    rewrite opp_opp in H. simpl in H, Cmn1. symmetry in Cmn1.
    right. split; assumption.

    simpl in m_min. rewrite succ_pred in m_min.
    simpl in m_max. rewrite pred_succ in m_max.

    set (Hcon := lte_definite m 0 m_max m_min).
    rewrite Hcon, multiply_zero in H. discriminate.
  Qed.

  Lemma eq_implies_multiply_eq_l : forall (i j k : Int),
    (i = j -> k * i = k * j).
  Proof.
    intros. rewrite H. reflexivity.
  Qed.

  Lemma eq_implies_multiply_eq_r : forall (i j k : Int),
    (i = j -> i * k = j * k).
  Proof.
    intros. rewrite H. reflexivity.
  Qed.

  Lemma eq_multiply_implies_eq_l : forall (i j k : Int),
    k <> 0 -> k * i = k * j -> i = j.
  Proof.
    intros i j k Hkz H.
    generalize (eq_implies_add_inv _ _ H).
    intro. rewrite <- multiply_distr_sub in H0.
    destruct (product_zero_implies_zero _ _ H0).
    contradiction.
    apply add_inv_implies_eq in H1. assumption.
  Qed.

  Lemma eq_multiply_implies_eq_r : forall (i j k : Int),
    k <> 0 -> i * k = j * k -> i = j.
  Proof.
    intros.
    rewrite (multiply_comm i k) in H0.
    rewrite (multiply_comm j k) in H0.
    apply (eq_multiply_implies_eq_l _ _ _ H H0).
  Qed.

  Inductive mod : Int -> Int -> Int -> Prop  := (*mod n a r ⇔ a ≡ r mod n*)
  | mod_id : forall (n : Int), mod n 0 0
  | mod_zero : forall (a : Int), mod 0 a a
  | mod_cycle : forall (n a r m : Int), (mod n a r) -> (mod n a (r + m*n)).

  Notation "a ≡ r mod n" := (mod n a r) (at level 90, no associativity): Int_scope.

  Fixpoint iterate_fn {T : Type} (f : T -> T) (n : Nat) (t : T) : T :=
  match n with
  | nat_zero => t
  | nat_succ n' => f (iterate_fn f n' t)
  end.

  Set Printing Coercions.

  Inductive Int' : Set :=
  | z0 : Int'
  | zpos : PosZ -> Int'
  | zneg : PosZ -> Int'.

  Definition Z'succ (n : Int') : Int' :=
  match n with
  | z0 => zpos pz_one
  | zpos n' => zpos (pz_succ n')
  | zneg n' => match n' with
               | pz_one => z0
               | pz_succ m => zneg m
               end
  end.

  Definition Z'pred (n : Int') : Int' :=
  match n with
  | z0 => zneg pz_one
  | zpos n' => match n' with
               | pz_one => z0
               | pz_succ m => zpos m
               end
  | zneg n' => zneg (pz_succ n')
  end.

  Definition Z'opp (n : Int') : Int' :=
  match n with
  | z0 => z0
  | zpos n' => zneg n'
  | zneg n' => zpos n'
  end.

  Definition inject_Int'_Int (n : Int') :=
  match n with
  | z0 => zero
  | zpos m => iterate_fn succ m zero
  | zneg m => iterate_fn pred m zero
  end.

  Fixpoint inject_Int_Int' (n : Int) :=
  match n with
  | zero => z0
  | succ n' => Z'succ (inject_Int_Int' n')
  | pred n' => Z'pred (inject_Int_Int' n')
  end.

  Theorem surjection_Int_Int' : forall (n : Int'), exists (m : Int),
    n = inject_Int_Int' m.
  Proof.
    intro. unfold inject_Int_Int'. induction n.
    exists zero. reflexivity.
    exists p. induction p. trivial.
    simpl. rewrite <- IHp. trivial.
    exists (- p). induction p. trivial.
    simpl. rewrite <- IHp. trivial.
  Qed.

  Lemma Z'succ_zpos : forall n : PosZ,
    Z'succ (zpos n) = zpos (pz_succ n).
  Proof.
    auto.
  Qed.

  Lemma Z'pred_zneg : forall n : PosZ,
    Z'pred (zneg n) = zneg (pz_succ n). (*n - 1 = - *)
  Proof.
    auto.
  Qed.

  Lemma Z_Z'_succ : forall (n : Int) (m : Int'),
    n = inject_Int'_Int m -> m = inject_Int_Int' n ->
    succ n = inject_Int'_Int (Z'succ m).
  Proof.
    intros. induction m; simpl.
    rewrite H. trivial.
    simpl in H. rewrite H. reflexivity.
    rewrite H.
    induction p;
    simpl; rewrite succ_pred; reflexivity.
  Qed.

  Lemma Z'_Z_succ : forall (n : Int) (m : Int'),
    n = inject_Int'_Int m -> m = inject_Int_Int' n ->
    inject_Int_Int' (succ n) = Z'succ m.
  Proof.
    intros. induction m; simpl;
    rewrite <- H0; reflexivity.
  Qed.

  Lemma Z_Z'_pred : forall (n : Int) (m : Int'),
    n = inject_Int'_Int m -> m = inject_Int_Int' n ->
    pred n = inject_Int'_Int (Z'pred m).
  Proof.
    intros. induction m; simpl.
    rewrite H. trivial.
    induction p; rewrite H;
    simpl; rewrite pred_succ; reflexivity.
    simpl in H. rewrite <- H. reflexivity.
  Qed.

  Lemma Z'_Z_pred : forall (n : Int) (m : Int'),
    n = inject_Int'_Int m -> m = inject_Int_Int' n ->
    inject_Int_Int' (pred n) = Z'pred m.
  Proof.
    intros. induction m; simpl;
    rewrite <- H0; reflexivity.
  Qed.

  Theorem surjection_Z'_Z : forall (n : Int), exists (m : Int'),
    n = inject_Int'_Int m.
  Proof.
    intro. induction n.
    exists z0. trivial.

    destruct IHn. exists (Z'succ x).
    unfold Z'succ. rewrite H.
    induction x; try trivial.
    unfold inject_Int'_Int, iterate_fn.
    destruct p; simpl; rewrite succ_pred; reflexivity.

    destruct IHn. exists (Z'pred x).
    unfold Z'pred. rewrite H.
    induction x; try trivial.
    unfold inject_Int'_Int, iterate_fn.
    destruct p; simpl; rewrite pred_succ; reflexivity.
  Qed.

  Theorem coercion_Z'_Z_Z'_id : forall (n : Int'),
    n = inject_Int_Int' (inject_Int'_Int n).
  Proof.
    intros. induction n. trivial.

    induction p. trivial.
    simpl. rewrite <- Z'succ_zpos.
    apply f_equal with (f := fun t => Z'succ t).
    rewrite IHp. trivial.

    induction p. trivial.
    simpl. rewrite <- Z'pred_zneg.
    apply f_equal with (f := fun t => Z'pred t).
    rewrite IHp. trivial.
  Qed.

  Theorem coercion_Z_Z'_Z_id : forall (n : Int),
    n = inject_Int'_Int (inject_Int_Int' n).
  Proof.
    intros. induction n;
    simpl; try (apply Z_Z'_succ || apply Z_Z'_pred); trivial.
  Qed.

  Theorem Int_Int'_coercion_equiv : forall n m,
    inject_Int_Int' n = m <-> inject_Int'_Int m = n.
  Proof.
    split; intro;
    induction H; symmetry;
    apply coercion_Z'_Z_Z'_id || apply coercion_Z_Z'_Z_id.
  Qed.

  Coercion inject_Int'_Int : Int' >-> Int.
  Coercion inject_Int_Int' : Int >-> Int'.

  Lemma Z_Z'_eq_succ : forall (n : Int) (m : Int'),
    n = m -> succ n = Z'succ m /\ succ m = Z'succ n.
  Proof.
    intros. split. rewrite Z_Z'_succ with (m := n).
    rewrite H. rewrite <- coercion_Z'_Z_Z'_id. trivial.
    rewrite <- coercion_Z_Z'_Z_id. trivial.
    trivial.

    rewrite Z_Z'_succ with (m := n).
    rewrite H. rewrite <- coercion_Z'_Z_Z'_id. trivial.
    symmetry. rewrite <- coercion_Z_Z'_Z_id. trivial.
    rewrite <- coercion_Z'_Z_Z'_id.
    apply Int_Int'_coercion_equiv. symmetry. trivial.
  Qed.

  Lemma Z_Z'_eq_pred : forall (n : Int) (m : Int'),
    n = m -> pred n = Z'pred m /\ pred m = Z'pred n.
  Proof.
    intros. split. rewrite Z_Z'_pred with (m := n).
    rewrite H. rewrite <- coercion_Z'_Z_Z'_id. trivial.
    rewrite <- coercion_Z_Z'_Z_id. trivial.
    trivial.

    rewrite Z_Z'_pred with (m := n).
    rewrite H. rewrite <- coercion_Z'_Z_Z'_id. trivial.
    symmetry. rewrite <- coercion_Z_Z'_Z_id. trivial.
    rewrite <- coercion_Z'_Z_Z'_id.
    apply Int_Int'_coercion_equiv. symmetry. trivial.
  Qed.

  Lemma Z_Z'_eq_opp : forall (n : Int),
    Zopp n = Z'opp n.
  Proof.
    intros. induction n. trivial.
  Qed.

  Definition Zsign (n : Int') :=
  match n with
  | z0 => zero
  | zpos n' => succ zero
  | zneg n' => pred zero
  end.

  Lemma PosZ_pos : forall n, positive (zpos n).
  Proof.
    intros. induction n.
    apply (lte_id 1).
    rewrite <- Z'succ_zpos.
    rewrite <- Z_Z'_succ with (n := zpos n).
    apply lte_s, IHn. reflexivity.
    rewrite <- coercion_Z'_Z_Z'_id. reflexivity.
  Qed.

  Theorem abs_product_Zsign : forall (n : Int'), abs n = n * (Zsign n).
  Proof.
    intros. destruct_sign n.
    trivial. destruct n.
    simpl.
  Qed.

  Theorem pos_zpos : forall n, positive n <-> exists m, n = zpos m.
  Proof.
    split. intro. induction H.
    exists pz_one. trivial.
    destruct IHlte. exists (pz_succ x).
    rewrite <- Z'succ_zpos, H0. trivial.

    intro. destruct H. induction x.
    simpl in H. rewrite H. apply (lte_id 1).
    rewrite H, <- Z'succ_zpos.
    rewrite <- Z_Z'_succ with (n := zpos x).
    apply lte_s.
  Qed.

  Record Q : Set := Q_make {Q_num : Int; Q_den : PosZ}.

  Declare Scope Q_scope.
  Delimit Scope Q_scope with Q.
  Bind Scope Q_scope with Q.
  Open Scope Q_scope.

  Infix "a # b" := (Q_make a b) (at level 55, no associativity) : Q_scope.

  Definition inject_Int_Q (n : Int) : Q := Q_make n pz_one.

  Coercion inject_Int_Q : Int >-> Q.

  Definition Q_eq (p q : Q) := (Q_num p * Q_den q) = (Q_num q * Q_den p).
  Definition Q_lte (p q : Q) := lte (Q_num p * Q_den q) (Q_num q * Q_den p).
  Definition Q_lt (p q : Q) := lt (Q_num p * Q_den q) (Q_num q * Q_den p).
  Definition Q_gte (p q : Q) := gte (Q_num p * Q_den q) (Q_num q * Q_den p).
  Definition Q_gt (p q : Q) := gt (Q_num p * Q_den q) (Q_num q * Q_den p).

  Infix "==" := Q_eq (at level 70, no associativity) : Q_scope.
  Infix "<" := Q_lt : Q_scope.
  Infix "<=" := Q_lte : Q_scope.
  Notation "x > y" := (Q_lt y x)(only parsing) : Q_scope.
  Notation "x >= y" := (Q_lte y x)(only parsing) : Q_scope.
  Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
  Notation "x <= y < z" := (x<=y/\y<z) : Q_scope.
  Notation "x < y <= z" := (x<y/\y<=z) : Q_scope.
  Notation "x < y < z" := (x<y/\y<z) : Q_scope.

  Hint Unfold Q_eq Q_lt Q_lte : hdb.

  Theorem Q_identity_weak : forall (p : Q), p == Q_make (Q_num p) (Q_den p).
  Proof.
    intro. unfold Q_eq. simpl. reflexivity.
  Qed.

  Lemma inject_Int_Q_injection : forall a b : Int, a == b -> a = b.
  Proof.
    intros a b H. unfold Q_eq in H. simpl in H.
    repeat rewrite multiply_id_r in H. assumption.
  Qed.

  Lemma Q_cancellation_l : forall (a : Int) (b m : PosZ),
    (Q_make a b) == (Q_make (m * a) (PosZmultiply m b)).
  Proof.
    intros. unfold Q_eq. simpl.
    rewrite PosZmultiply_Zmultiply_coincide. ring.
  Qed.

  Lemma Q_eq_refl : forall (p : Q), p == p.
  Proof.
    auto with hdb.
  Qed.

  Lemma Q_eq_symm : forall (p q : Q), p == q -> q == p.
  Proof.
    auto with hdb.
  Qed.

  Lemma Q_eq_trans : forall (p q r : Q), p == q -> q == r -> p == r.
  Proof.
    unfold Q_eq. intros p q r H G.
    apply eq_multiply_implies_eq_l with (k := Q_den q).
    apply PosZ_not_Int_zero.
    transitivity (Q_num p * Q_den q * Q_den r); try ring.
    rewrite H.
    transitivity (Q_num q * Q_den r * Q_den p); try ring.
    rewrite G.
    ring.
  Qed.

  Hint Resolve Q_eq_refl : hdb.
  Hint Resolve Q_eq_symm : hdb.
  Hint Resolve Q_eq_trans : hdb.

  Instance Q_Setoid : Equivalence Q_eq.
  Proof.
    split; red; eauto with hdb.
  Qed.

  Definition Q_add (p q : Q) :=
    Q_make ((Q_num p) * (Q_den q) + (Q_num q) * (Q_den p))
           (PosZmultiply (Q_den p) (Q_den q)).

  Definition Q_mul (p q : Q) :=
    Q_make ((Q_num p) * (Q_num q)) (PosZmultiply (Q_den p) (Q_den q)).

  Definition Q_sub (p q : Q) :=
    Q_make ((Q_num p) * (Q_den q) - (Q_num q) * (Q_den p))
           (PosZmultiply (Q_den p) (Q_den q)).

  Definition Q_opp (p : Q) := Q_make (- (Q_num p)) (Q_den p).

  Definition Q_inv (p : Q) :=
  match Q_num p with
  | zero => zero
  | _ => match
  end.

  Definition Q_div (p q : Q) := Q_mul p (Q_inv q).

  Infix "⊕" := Q_add (at level 50, no associativity) : Q_scope.
  Infix "⊗" := Q_mul (at level 50, no associativity) : Q_scope.
  Notation "- p" := (Q_opp p).

  Lemma Q_add_id_r : forall p : Q, p ⊕ 0 = p.
  Proof.
    intros. unfold Q_add. simpl.
    repeat rewrite multiply_id_r. rewrite add_zero_r.
    symmetry. apply Q_identity.

  Qed.

author: felixjhb


text:
(*|
.. default-role:: math

.. role:: m(math)

The traditional process for developing a verified compiler is to define types that model the source (`S`) and target (`T`) languages, and to write a function `f: S → T` that transforms an instance `s` of the source type into an instance `t = f(s)` of the target type, such all behaviors of `t` match existing behaviors of `s` (“refinement”) and sometimes additionally such that all behaviors of `s` can be achieved by `t` (“equivalence”, or “correctness”).

Naturally, *proving* correctness for such a compiler requires a formal understanding of the *semantics* of languages `S` and `T` (that is, a way to give meaning to programs `s ∈ S` and `t ∈ T`, so that it is possible to speak of the behaviors of a program: return values, I/O, resource usage, etc.).  Then the refinement criterion above translates to `σ_T(t) ⊆ σ_S(s)` (where `σ_S(s)` denotes the behaviors of `s` and `σ_T(t)` those of `t`), and the correctness criterion defines a relation `∼` between source and target programs such that `t ∼ s` iff `σ_T(t) = σ_S(s)`.  With that, a compiler `f` is correct iff `f(s) ∼ s` for all `s`.

Relational compilation is a twist on that approach: it turns out that instead of writing the compiler as a monolithic program and separately verifying it, we can break up the compiler's correctness proof into a collection of orthogonal correctness theorems and *use these theorems* to drive a code-generating proof-search process.  It is a Prolog-style “compilers as relations” approach but taken one step further to get “compilers as (constructive) decision procedures”.

Instead of writing our compiler as a function `f: S → T`, we will write the compiler as a (partial) decision procedure: an automated proof-search process for proving theorems of the form `∃\: t.\; σ_T(t) = σ_S(s)`.  In a constructive setting, any proof of that statement must exhibit a witness `t`, which will be the (correct) compiled version of `s`.  (Note that the theorem does not `∀`-quantify `s`, as we want to generate one distinct proof *per input program* — otherwise, with a `∀ s` quantification, the theorem would be equivalent by skolemization to `∃\: f.\; ∀ s, σ_T(f(s)) = σ_S(s)`, which is the same as defining a single compilation function `f`… and precisely what we're trying to avoid.)

The two main benefits of this approach are flexibility and trustworthiness: it provides a very natural and modular way to think of compiler extensions, and it makes it possible to extract shallowly embedded programs without trusting an extraction routine (in contrast, extraction in Coq is trusted).  The main cost?  Completeness: a (total) function always terminates and produces a compiled output; a (partial) proof-search process may loop or fail to produce an output. [#]_

This is not an entirely new idea: variations on this trick have been variously referred to in the literature as *proof-producing compilation*, *certifying compilation*, and, when the source language is shallowly embedded (we will get to that a bit later), *proof-producing extraction*, *certifying extraction*, or *binary extraction*.  I like to call this style of compilation “relational compilation”, and to explain it I like to start from a traditional verified compiler and progressively derive a relational compiler from it.

.. [#] Of course things are not so clear-cut: a compiler may be written as a partial function that sometimes fails to compile input programs, like ill-typed programs in OCaml, programs with too-deep template recursion in C++, programs with too-long lines in Python, etc. — but the extensibility of relational compilers also tends to make them more susceptible to incompleteness, and since they're written in meta-language it is often not easy or even possible to prove their completeness.

~~~~~~~~~~

.. coq:: none
|*)

From Ltac2 Require Ltac2.

From Coq Require Import String.
From Coq Require Import List ZArith Derive.
Import ListNotations.

Open Scope string_scope.
Open Scope list_scope.
Open Scope Z_scope.

Implicit Type z : Z.
Implicit Type str : string.

(*|
A step-by-step example
----------------------

.. coq:: none
|*)

Arguments exist [A] {_} _ {_}.
Arguments ex_intro [A] {_} _ {_}.
Notation "'type' 'of' x" := ((fun A (_: A) => A) _ x) (at level 0).
Set Warnings "-deprecated-hint-without-locality".

Tactic Notation "eauto" "with" ident(db) :=
  typeclasses eauto with db.

Module Arith.

(*|
Here is a concrete pair of languages that we will use as a demonstration.  Language `S` is a simple arithmetic-expressions language.  Language `T` is a trivial stack machine.

..
   You can `download the Coq code of this example <relational-compilation.v>`__.

.. default-role:: coq

Language definitions
~~~~~~~~~~~~~~~~~~~~

On the left is the Coq definition of `S`, with only three constructors: constants, negation, and addition; on the right is the definition of `T`: a program in `T` is a list of stack operations `T_Op`, which may be pushing a constant, popping the two values on the top of the stack and pushing their difference, or popping the two values on the top of the stack and pushing their sum.

.. compound::
   :class: sidebyside

   .. container:: narrowside

      .. coq::
|*)

Inductive S :=
| SInt z
| SOpp (s : S)
| SAdd (s1 s2 : S).
Implicit Type s : S. (* .none *)

(*|
      .. coq:: none
|*)

(*
Notation "$ z" := (SInt z) (at level 34, format "$ z").
Notation "$- z" := (SOpp z) (at level 35, format "$- z").
Infix "$+" := SAdd (at level 50, left associativity).
*)

(*|
   .. container:: wideside

      .. coq::
|*)

Inductive T_Op :=
| TPush z
| TPopSub
| TPopAdd.
Implicit Type op : T_Op. (* .none *)

Definition T := list T_Op.
Implicit Type t : T. (* .none *)

(*|
Concretely, a program in ``S`` might be `SAdd (SInt 3) (SInt 4)`, which computes the sum of the constants `3` and `4`.  A corresponding program in `T` would be `[TPush 3; TPush 4; TPopAdd]`, which pushes the constants `3` and `4` and then places their sum on the stack.

Semantics
~~~~~~~~~
The semantics of these languages are easy to define using interpreters.  On the left, operations on terms in `S` are mapped to corresponding operations on :m:`ℤ`, producing an integer.  On the right, stack operations are interpreted one by one, starting from a stack and producing a new stack.

.. compound::
   :class: sidebyside

   .. container:: narrowside

      .. coq::
|*)

Fixpoint σS s : Z :=
  match s with
  | SInt z     => z
  | SOpp s     => - σS s
  | SAdd s1 s2 => σS s1 + σS s2
  end.

(*|
   .. container:: wideside

      .. coq::
|*)

Notation Stack := (list Z).

Definition σOp (ts: Stack) op : Stack :=
  match op, ts with
  | TPush n, ts => n :: ts
  | TPopAdd, n2::n1::ts => n1+n2 :: ts
  | TPopSub, n2::n1::ts => n1-n2 :: ts
  | _, ts => ts (* Invalid: no-op *)
  end.

Definition σT t (ts: Stack) : Stack :=
  List.fold_left σOp t ts.

(*|
With these definitions, program equivalence is straightforward to define (the definition is contextual, in the sense that it talks about equivalence in the context of a non-empty stack):
|*)

Module DeepEmbedded. (* .none *)
Notation "t ∼ s" := (forall ts, σT t ts = σS s :: ts)
  (at level 70).

(*|
Compilation
~~~~~~~~~~~

In the simplest case, a compiler is a single recursive function; more typically, a compiler is engineered as a sequence (composition) of passes, each responsible for a well-defined task: typically, either an *optimization* (within one language, intended to improve performance of the output) or *lowering* (from one intermediate language to another, intended to bring the program closer to its final form), though these boundaries are porous.  Here is a simple one-step compiler for our pair of languages:
|*)

Fixpoint StoT s := match s with
  | SInt z     => [TPush z]
  | SOpp s     => [TPush 0] ++ StoT s ++ [TPopSub]
  | SAdd s1 s2 => StoT s1 ++ StoT s2 ++ [TPopAdd]
end.

(*|
The `SInt` case maps to a stack-machine program that simply pushes the constant `z` on the stack; the `SOpp` case returns a program that first puts a 0 on the stack, then computes the value corresponding to the operand `s`, and finally computes the subtraction of these two using the `TPopSub` opcode; and the `SAdd` case produces a program that pushes both operands in succession before computing their sum using the `TPopAdd` opcode.

The Coq command ``Compute`` lets us run this compiler and confirm that it seems to operate correctly:
|*)

Example s7 :=
  SAdd (SAdd (SInt 3) (SInt 6))
       (SOpp (SInt 2)).

(*|
- Running the example program `s7` directly
  returns `7`:
|*)

Compute σS s7. (* .unfold *)

(*|
- Compiling the program and then running it produces the same result (a stack with a single element, `7`):

  .. coq::
|*)

Compute StoT s7. (* .unfold *)
Compute σT (StoT s7) []. (* .unfold *)

(*|
Compiler correctness
~~~~~~~~~~~~~~~~~~~~

Of course, one example is not enough to establish that the compiler above works; instead, here is a proof of its correctness, which proceeds by induction with three cases:

.. coq::
   :name: fn-ok
|*)

Lemma StoT_Rok : forall s, StoT s ∼ s.
Proof.
  induction s.
  all: intros; unfold σT; simpl.
  - (* `SInt` case *)
    reflexivity.
  - (* `SOpp` case *)
    rewrite fold_left_app.
    rewrite IHs.
    reflexivity.
  - (* `SAdd` case *)
    rewrite !fold_left_app.
    rewrite IHs1, IHs2.
    reflexivity.
Qed.

(*|
This compiler operates in a single pass, but arguably even a small compiler like this one could benefit from a multi-pass approach: for example, we might prefer to separate lowering into two phases translating all unary `SOpp` operations to a new binary operator `SSub` (`SOpp x → SSub (Sconst 0) x`) in a first pass, and dealing with stack operations in a second pass.

Compiling with relations
~~~~~~~~~~~~~~~~~~~~~~~~

We will observe two things about `StoT` and its proof.

First, `StoT`, like any function, can be rewritten as a relation (any function :m:`f: x ↦ f(x)` defines a relation :m:`∼_f` such that :m:`t ∼_f s` iff :m:`t = f(s)`; this relation is sometimes called the graph of the function).  Here is one natural way to rephrase `StoT` as a relation `ℜ`; notice how each branch of the recursion maps to a case in the inductive definition of the relation (each constructor defines an introduction rule for `ℜ`, which corresponds to a branch in the original recursion, and each `x ℜ y` premise of each case corresponds to a recursive call to the function):
|*)

Reserved Notation "t 'ℜ' s"
  (at level 68, no associativity). (* .none *)
Inductive StoT_rel : T -> S -> Prop :=
| StoT_RNat : forall z,
    [TPush z] ℜ SInt z
| StoT_ROpp : forall t s,
    t ℜ s ->
    [TPush 0] ++ t ++ [TPopSub] ℜ SOpp s
| StoT_RAdd : forall t1 s1 t2 s2,
    t1 ℜ s1 ->
    t2 ℜ s2 ->
    t1 ++ t2 ++ [TPopAdd] ℜ SAdd s1 s2
where "t 'ℜ' s" := (StoT_rel t s).

(*|
Now, what does correctness mean for `StoT`?  Correctness for this compilation relation is… just a subset relation:

   The relation `ℜ` is a *correct* compilation relation for languages :m:`S` and :m:`T` if its graph is a subset of the graph of :m:`∼`.

This condition is sufficient: any relation that is a subset of :m:`∼` defines a correct (possibly one-to-many, possibly suboptimal, but *correct*\ ) mapping from source programs to destination programs.

And indeed, the relation above is a correct compilation relation:

.. coq::
   :name: rel-ok
|*)

Theorem StoT_rel_ok : forall t s,
    t ℜ s -> t ∼ s.
Proof.
  induction 1.
  all: intros; unfold σT; simpl. (* .fold *)
  - (* `StoT_RNat` case *)
    reflexivity.
  - (* `StoT_ROpp` case *)
    rewrite fold_left_app.
    rewrite IHStoT_rel.
    reflexivity.
  - (* `StoT_RAdd` case *)
    rewrite !fold_left_app.
    rewrite IHStoT_rel1, IHStoT_rel2.
    reflexivity.
Qed.

(*|
Now that we have `ℜ`, we can use it to prove equivalences for specific programs: for example, we can write a proof to show specifically that the compiled version of our example program `s7` matches the original `s7` by applying each of the constructors of the relation `ℜ` one by one:
|*)

Goal ([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++
     ([TPush 0] ++ [TPush 2] ++ [TPopSub]) ++
     [TPopAdd] ℜ
     SAdd (SAdd (SInt 3) (SInt 6))
     (SOpp (SInt 2)).
Proof.
  apply StoT_RAdd. (* .unfold *)
  - apply StoT_RAdd. (* .unfold *)
    + apply StoT_RNat.
    + apply StoT_RNat.
  - apply StoT_ROpp. (* .unfold *)
    + apply StoT_RNat.
Qed.

(*|
Now, how can we use this relation to *run* the compiler instead?  By using proof search!  This is standard practice in the world of logic programming.  To *compile* our earlier program `s7`, for example, we can simply search for a program `t7` such that `t7 ℜ s7`, which in Coq terms looks like this:
|*)

Example t7_rel: { t7 | t7 ℜ s7 }.
Proof.
  unfold s7; eexists. (* .unfold *)

(*|
Now the goal includes an indeterminate value `?t7`, called an existential variable (\ *evar*\ ), corresponding to the program that we are attempting to derive, and each application or a lemma *refines* that evar by plugging in a partial program:
|*)

  apply StoT_RAdd. (* .unfold *)

(*|
After applying the lemma `StoT_RAdd`, we are asked to provide two subprograms, each corresponding to one operand of the addition:
|*)

  - apply StoT_RAdd. (* .unfold *)
    + apply StoT_RNat.
    + apply StoT_RNat.
  - apply StoT_ROpp. (* .unfold *)
    + apply StoT_RNat.
Defined.

(*|
We get the exact same program, but this time instead of *validating* a previous compilation pass, we have generated the program from scratch:
|*)

Compute t7_rel. (* .unfold *)

(*|
We can also use Coq's inspection facilities to see the proof term as it is being generated (this time the boxes show the internal proof term, not the goals):

.. coq:: none
|*)

Goal { t7 | t7 ℜ s7 }. (* .none *)
Proof.
  unfold s7; eexists.

(*|
.. coq:: unfold in
|*)

  Show Proof. (* .messages .no-in *)
  apply StoT_RAdd. (* .in *)
  Show Proof. (* .messages .no-in *)
  - apply StoT_RAdd.
    Show Proof. (* .messages .no-in *)
    + apply StoT_RNat.
      Show Proof. (* .messages .no-in *)
    + apply StoT_RNat.
      Show Proof. (* .messages .no-in *)
  - apply StoT_ROpp.
    Show Proof. (* .messages .no-in *)
    + apply StoT_RNat.
      Show Proof. (* .messages .no-in *)
Defined. (* .none *)

(*|
This derivation shows how the program gets built: each lemma application is equivalent to one recursive call in a run of the compilation function `StoT`.

Coq has facilities to perform proof search automatically using a set of lemmas, which we can use to automate the derivation of `t7`: it suffices to register all constructors of `ℜ` in a “hint database”, as follows: [#]_

.. [#] In the following we use ``eauto`` as an abbreviation for ``typeclasses eauto``, a more flexible version of Coq's ``eauto`` tactic.  In particular, using ``typeclasses eauto`` allows us to specify priorities on lemmas.
|*)

Create HintDb cc.
Hint Resolve exist : cc. (* .none *)
Hint Constructors StoT_rel : cc.

Example t7_rel_eauto: { t7 | t7 ℜ s7 }.
Proof. eauto with cc. Defined.

Compute t7_rel_eauto. (* .unfold *)

(*|
And of course, the result is *correct-by-construction*, in the sense that it carries its own proof of correctness:
|*)

Eval cbn in type of (proj2_sig t7_rel_eauto). (* .unfold *)

(*|
This is traditional *logic programming*, applied to compilers.  We have now learned one fact:

   Correctly compiling a program :m:`s` is the same as proving :m:`∃\: t.\; t ∼ s`.

Open-ended compilation
~~~~~~~~~~~~~~~~~~~~~~

The proofs of correctness for the functional version of the compiler (`StoT`, :mref:`.io#fn-ok.s(Proof)`) and for the relational version (`StoT_rel`, :mref:`.io#rel-ok.s(Proof)`) have the exact same structure.  They are both composed of three orthogonal lemmas:

.. class:: tight-list

1. .. mquote:: .io#rel-ok.s(induction).g#1.ccl
2. .. mquote:: .io#rel-ok.s(induction).g#2.ccl
3. .. mquote:: .io#rel-ok.s(induction).g#3.ccl

Each of these is really a standalone fact, and each corresponds to a *partial* relation between :m:`S` and :m:`T`, each connecting *some* programs in :m:`S` to *some* programs in :m:`T`.  In other words:

   A relational compiler is really just a collection of facts connecting programs in the target language to programs in the source language.

This means that we don't even need to define a relation.  Instead, we can have three lemmas that directly refer to the original equivalence `~`:
|*)

Lemma StoT_Int z :
    [TPush z] ∼ SInt z.

(*|
.. coq:: none
|*)

Proof. reflexivity. Qed.

(*||*)

Lemma StoT_Opp t s :
    t ∼ s ->
    [TPush 0] ++ t ++ [TPopSub] ∼ SOpp s.

(*|
.. coq:: none
|*)

Proof.
  unfold σT; simpl; intros * IH *.
  rewrite fold_left_app, IH.
  reflexivity.
Qed.

(*||*)

Lemma StoT_Plus t1 s1 t2 s2 :
    t1 ∼ s1 ->
    t2 ∼ s2 ->
    t1 ++ t2 ++ [TPopAdd] ∼ SAdd s1 s2.

(*|
.. coq:: none
|*)

Proof.
  unfold σT; simpl; intros * IH1 IH2 *.
  rewrite !fold_left_app, IH1, IH2.
  reflexivity.
Qed.

(*|
And from these, we can build a compiler!  We just need to place all these facts into a new database of lemmas, which Coq will use as part of its proof search:
|*)

Create HintDb c.
Opaque σS σT.
Hint Resolve exist : c. (* .none *)
Hint Resolve StoT_Int : c.
Hint Resolve StoT_Opp : c.
Hint Resolve StoT_Plus : c.

(*|
And then we can derive compiled programs and their proofs:
|*)

Example t7_fn_eauto: { t7 | t7 ∼ s7 }.
Proof. eauto with c. Defined.

Compute t7_fn_eauto. (* .unfold *)

(*|
.. sidebar:: _`Box 1` — Opacity

   Making `σS` and `σT` *opaque* prevents commands like ``eauto`` from unfolding our definitions too aggressively.  Without it, since our example language :m:`S` is so simple that all programs are actually just constants (!), our new compiler would just reduce programs before compiling them:
|*)

Transparent σS σT.
Example t7_fn_eauto_t: { t7 | t7 ∼ s7 }. Proof. eauto with c. Defined.
Compute t7_fn_eauto_t. (* .unfold *)
End DeepEmbedded. (* .none *)

(*|
   The alternative would be to give priority to `StoT_Opp` and `StoT_Plus` over `StoT_int`, which we demonstrate later in this document.

   .. massert::

      .s(Compute).msg{*TPush 7*}

That is the core idea of relational compilation.  On this simple example it looks mostly like an odd curiosity, but it is actually very useful for compiling (shallowly) embedded domain-specific languages (EDSLs), especially when the compiler needs to be extensible.

Use case 1: Compiling shallowly embedded DSLs
---------------------------------------------

.. coq:: none
|*)

Module ShallowEmbedded.

(*|
The original setup of the problem (compiling from language :m:`S` to language :m:`T`) required us to exhibit a function :m:`f: S → T`.  Not so with the new set up, which instead requires us to prove instances of the `∼` relation (one per program).  What this means is that we can apply this compilation technique to compile *shallowly* embedded programs, including shallowly embedded DSLs [#]_.

.. [#] A shallow embedding is one where programs are defined directly in the host language in contrast with a deep embedding where programs are represented as abstract syntax trees, i.e. data.

Here is how we would change our previous example to compile arithmetic expressions written directly in Gallina:

1. Start by redefining the relation to use *Gallina expressions* on the right side of the equivalence (there are no more references to :m:`S` nor ``σS``):

   .. coq::
|*)

Notation "t ≈ s" := (forall ts, σT t ts = s :: ts) (at level 68).

(*|
2. Add compilation lemmas (the proofs are exactly the same as before, so they are omitted).  Note that on the right side we have plain Gallina `+` and `-`, not `SAdd` and `SOp`, so each lemma now relates a shallow program to an equivalent deep-embedded one:

   .. coq::
|*)

Lemma GallinatoT_Z z :
  [TPush z] ≈ z.

(*|
   .. coq:: none
|*)

Proof. reflexivity. Qed.

(*||*)

Lemma GallinatoT_Zopp t z :
  t ≈ z ->
  [TPush 0] ++ t ++ [TPopSub] ≈ - z.

(*|
   .. coq:: none
|*)

Proof.
  unfold σT; simpl; intros * IH *.
  rewrite fold_left_app, IH.
  reflexivity.
Qed.

(*||*)

Lemma GallinatoT_Zadd t1 z1 t2 z2 :
  t1 ≈ z1 ->
  t2 ≈ z2 ->
  t1 ++ t2 ++ [TPopAdd] ≈ z1 + z2.

(*|
   .. coq:: none
|*)

Proof.
  unfold σT; simpl; intros * IH1 IH2 *.
  rewrite !fold_left_app, IH1, IH2.
  reflexivity.
Qed.

(*|
These lemmas are sufficient to create a small compiler: as before we populate a hint database with our compilation lemmas:
|*)

Create HintDb stack.
Hint Opaque Z.add Z.opp : stack. (* .none *)
Hint Resolve exist : stack. (* .none *)
Hint Resolve GallinatoT_Z | 10 : stack.
Hint Resolve GallinatoT_Zopp : stack.
Hint Resolve GallinatoT_Zadd : stack.

(*|
And then we run our relational compiler on shallowly embedded input programs:
|*)

Example g7 := 3 + 6 + Z.opp 2.

Example t7_shallow: { t7 | t7 ≈ g7 }.
Proof. eauto with stack. Defined.

Compute t7_shallow. (* .unfold *)

(*|
Of course, it is easy to package this process in a convenient notation (the pattern `match Set return T with _ => X end` is a roundabout way to force the type of the value `X`):
|*)

Notation compile gallina_term :=
  (match Set return { t | t ≈ gallina_term } with
   | _ => ltac:(eauto with stack)
   end)
  (only parsing).

Compute compile (3 + 6 + Z.opp 2). (* .unfold *)

(*|
There is something slightly magical happening here.  By rephrasing compilation as a proof search problem, we have been able to construct a compiler that would not even be expressible (let alone provable!) as a regular Gallina function.  Reasoning on shallowly embedded programs is often much nicer than reasoning on deeply embedded programs, and this technique offers a convenient way to bridge the gap.

.. coq:: none
|*)

End ShallowEmbedded.
End Arith.

author: mit-plv

repo: rupicola

save_path: github-repos/coq/mit-plv-rupicola


text:
From stdpp Require Import finite vector numbers.

Locate vec.
Compute vec.
Compute vec bool 1.
Compute [# true ; false ].

Class Vector (v : Type) (s : Type) :=
  {
    vsum : v -> v -> v;
    smul : s -> v -> v;
    vzero : v;
    dist : forall s x y, smul s (vsum x y) = vsum (smul s x) (smul s y)

  }.
Print Vector.

Require Import QArith.
Search Q.
Print Qmult.
Print Qmult'.
Print Scope Q_scope.

Instance zerovect {a} : Vector unit a. refine  {|
                                          vsum x y := tt;
                                          smul _ _ := tt;
                                          vzero := tt

                                         |}.
intros. auto. Qed.

Search ring_theory.

Goal forall y z,  (Qplus y z) = (Qplus z y). intros. Search (_ + _). apply Qplus_comm.

Instance qvect : Vector Q Q. refine {|
                                vsum := Qplus;
                                smul := Qmult;
                                vzero := 0
                               |}.
intros. ring.

Instance tupvect `{Vector v s}  : Vector (v * v) s := {|
                                                       vsum u w := match u,w with (x,y), (a,b) => (vsum x a, vsum y b) end;
                                                       smul s v := match v with (x,y) => (smul s x, smul s y) end;
                                                       vzero := (vzero, vzero)

                                                     |}.
(*
Instance arrvect {a} `{Vector s s} : Vector (a -> s) s := {|
                                                vsum u w := fun z => vsum (u z) (w z) ;
                                                smul s v := fun z => smul s (v z) ;
                                                vzero := ?

                                                |}.
*)
Class Norm (v : Type) (s : Type) :=
  {
    norm : v -> s
    }.

Search Q.
(* Instance qnorm : Norm Q Q :=
  {|
    norm := Qabs
    |}.
 *)

Class Inner (v : Type) (s : Type) :=
  {
    dot : v -> v ->  s
  }.

 Instance dotQ : Inner Q Q :=
  {|
    dot := Qmult
    |}.

 Instance tupQ `{Inner a Q} `{Inner b Q} : Inner (a * b) Q :=
  {|
    dot x y := match x, y with | (a,b),(c,d) => (dot a c) + (dot b d) end
  |}.

Print nat.

Fixpoint vec n a : Type := match n with | S n' => (a * (vec n' a)) | O => unit end.

Compute vec 10 Q.

Definition norm2 `{Inner v s} (x : v) := dot x x.

(* Instance sumvect `{Vector v s} `{Vector w s} := Vector (v + w) s := {|
                                                                    vsum

                                                                    |}.
Nope, that's silly.

Thes definitions make it rather difficult to define kroncker product.
I guess
class Kron a b c s := {
   kron : a -> b -> c
}

 *)
Class Kron (a b c : Type) := {
   kron : a -> b -> c
                              }.

Instance scalarkron `{Vector b s} : Kron  s b b := {|
                                      kron := smul
                                                    |}.

Instance dsumkron `{Kron a c d} `{Kron b c e} :  Kron (prod a  b) c (d * e) := {|
                                kron x y := match x with | (a,b) => (kron a y, kron b y) end
                                (* : Vector d s *)
                                                                              |}.

Compute kron (vzero : (Q * Q) ) (vzero : (Q * Q)).

 Fixpoint e {a} n : vec n a. := match n with

(*

I definitely want to use the decidable typeclass technology.
???

Can I get psatz to fire on this stuff?

Decidable (a = a) for

What about Decision (smul s (vsum ) = )

We could write a Ring normalizer using typeclases

Class Ring a {
   mul : a -> a -> a;
   plus : a -> a -> a;
   zero : a -> a -> a;
   one : a -> a -> a;
   negate : a -> a
}

*)

repo: coq-vector


text:
Require Export GeoCoq.Elements.OriginalProofs.proposition_42.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_42B :
   forall B C D E J K R a b c e,
   Triangle a b c -> Midpoint b e c -> nCol J D K -> Midpoint B E C -> Cong E C e c -> nCol R E C ->
   exists X Z, PG X E C Z /\ EF a b e c X E C Z /\ CongA C E X J D K /\ OS R X E C.
Proof.
intros.
assert ((BetS B E C /\ Cong B E E C)) by (conclude_def Midpoint ).
assert ((BetS b e c /\ Cong b e e c)) by (conclude_def Midpoint ).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (nCol a b c) by (conclude_def Triangle ).
assert (nCol E C R) by (forward_using lemma_NCorder).
assert (Col B E C) by (conclude_def Col ).
assert (Col E C B) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col E C C) by (conclude_def Col ).
assert (nCol B C R) by (conclude lemma_NChelper).
rename_H H;let Tf:=fresh in
assert (Tf:exists P H, (Out B C H /\ CongA P B H a b c /\ OS P R B C)) by (conclude proposition_23C);destruct Tf as [P[H]];spliter.
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong E C B E) by (conclude lemma_congruencesymmetric).
assert (Cong E C e c) by (conclude lemma_congruencetransitive).
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong e c b e) by (conclude lemma_congruencesymmetric).
assert (Cong B E b e) by (conclude lemma_congruencetransitive).
assert (Cong B C b c) by (conclude cn_sumofparts).
assert (CongA a b c P B H) by (conclude lemma_equalanglessymmetric).
assert (Out B H C) by (conclude lemma_ray5).
assert (nCol B C P) by (conclude_def OS ).
assert (neq B P) by (forward_using lemma_NCdistinct).
assert (nCol a b c) by (conclude_def Triangle ).
assert (neq b a) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists A, (Out B P A /\ Cong B A b a)) by (conclude lemma_layoff);destruct Tf as [A];spliter.
assert (CongA a b c A B C) by (conclude lemma_equalangleshelper).
assert (CongA A B C a b c) by (conclude lemma_equalanglessymmetric).
assert (nCol A B C) by (conclude lemma_equalanglesNC).
assert (Triangle A B C) by (conclude_def Triangle ).
assert (Cong A C a c) by (conclude proposition_04).
assert (Cong A B a b) by (forward_using lemma_congruenceflip).
assert (Cong C A c a) by (forward_using lemma_congruenceflip).
assert (Cong E A e a) by (conclude lemma_interior5).
assert (Cong A E a e) by (forward_using lemma_congruenceflip).
assert (Cong E B e b) by (forward_using lemma_congruenceflip).
assert (Col B E C) by (conclude_def Col ).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (nCol B C A) by (forward_using lemma_NCorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (neq B E) by (forward_using lemma_betweennotequal).
assert (nCol B E A) by (conclude lemma_NChelper).
assert (nCol A E B) by (forward_using lemma_NCorder).
assert (Col b e c) by (conclude_def Col ).
assert (Col b c e) by (forward_using lemma_collinearorder).
assert (nCol b c a) by (forward_using lemma_NCorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col b c b) by (conclude_def Col ).
assert (neq b e) by (forward_using lemma_betweennotequal).
assert (nCol b e a) by (conclude lemma_NChelper).
assert (nCol a e b) by (forward_using lemma_NCorder).
assert (Triangle A E B) by (conclude_def Triangle ).
assert (Cong_3 A E B a e b) by (conclude_def Cong_3 ).
assert (ET A E B a e b) by (conclude axiom_congruentequal).
assert (Col C B E) by (forward_using lemma_collinearorder).
assert (neq E C) by (forward_using lemma_betweennotequal).
assert (neq C E) by (conclude lemma_inequalitysymmetric).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col C B C) by (conclude_def Col ).
assert (nCol C E A) by (conclude lemma_NChelper).
assert (nCol A E C) by (forward_using lemma_NCorder).
assert (Triangle A E C) by (conclude_def Triangle ).
assert (Cong_3 A E C a e c) by (conclude_def Cong_3 ).
assert (ET A E C a e c) by (conclude axiom_congruentequal).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col A E E) by (conclude_def Col ).
assert (TS B A E C) by (conclude_def TS ).
assert (eq e e) by (conclude cn_equalityreflexive).
assert (Col a e e) by (conclude_def Col ).
assert (TS b a e c) by (conclude_def TS ).
assert (EF A B E C a b e c) by (conclude axiom_paste3).
assert (EF a b e c A B E C) by (conclude axiom_EFsymmetric).
let Tf:=fresh in
assert (Tf:exists F G, (PG F E C G /\ EF A B E C F E C G /\ CongA C E F J D K /\ Col F G A)) by (conclude proposition_42);destruct Tf as [F[G]];spliter.
assert (EF a b e c F E C G) by (conclude axiom_EFtransitive).
assert (OS R P B C) by (forward_using lemma_samesidesymmetric).
assert (Col B B C) by (conclude_def Col ).
assert (OS R A B C) by (conclude lemma_sameside2).
assert (OS R A C B) by (conclude lemma_samesideflip).
assert (OS R A C E) by (conclude lemma_samesidecollinear).
assert (OS A R C E) by (forward_using lemma_samesidesymmetric).
assert (OS A R E C) by (conclude lemma_samesideflip).
assert (Col G F A) by (forward_using lemma_collinearorder).
assert (Par F G E C) by (conclude_def PG ).
assert (Par E C F G) by (conclude lemma_parallelsymmetric).
assert (Par E C G F) by (forward_using lemma_parallelflip).
assert (OS R F E C).
by cases on (eq A F \/ neq A F).
{
 assert (OS R A E C) by (conclude lemma_samesideflip).
 assert (OS R F E C) by (conclude cn_equalitysub).
 close.
 }
{
 assert (Par E C A F) by (conclude lemma_collinearparallel).
 assert (Par E C F A) by (forward_using lemma_parallelflip).
 assert (TP E C F A) by (conclude lemma_paralleldef2B).
 assert (OS F A E C) by (conclude_def TP ).
 assert (OS F R E C) by (conclude lemma_samesidetransitive).
 assert (OS R F E C) by (forward_using lemma_samesidesymmetric).
 close.
 }
(** cases *)
close.
Qed.

End Euclid.

author: GeoCoq

repo: GeoCoq

save_path: github-repos/coq/GeoCoq-GeoCoq


text:
(*
(C) Copyright 2010, COQTAIL team

Project Info: http://sourceforge.net/projects/coqtail/

This library is free software; you can redistribute it and/or modify it
under the terms of the GNU Lesser General Public License as published by
the Free Software Foundation; either version 2.1 of the License, or
(at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public
License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301,
USA.
*)

Require Export Reals.
Require Export Max.
Require Export Coq.omega.Omega.
Local Open Scope R_scope.

Definition strictly_increasing (f : nat -> nat) := forall n: nat, (f n < f (S n)) %nat.

(** Definition of a sub-sequence*)
Definition sub_seq (An : nat -> R) (f : nat -> nat) (pr : strictly_increasing f) :=
    fun n => An (f n).

Lemma sincr_ge_id (f : nat -> nat) : strictly_increasing f -> forall n : nat, (n <= f n )%nat.
Proof.
induction n.
omega.
apply le_trans with (S (f n)).
apply le_n_S.
apply IHn.
apply lt_le_S.
apply (H n).
Qed.

(** A sub-sequence of a convergent sequence converges to the same limit*)
Lemma Rsubseq_cv : forall (An : nat -> R) (f : nat -> nat) (pr : strictly_increasing f) (l : R),
    Un_cv An l -> Un_cv (sub_seq An f pr) l.
Proof.
unfold Un_cv.
intros An f pr l Hcv eps Heps.
destruct (Hcv eps Heps) as (N, HN).
exists N.
intros n Hn.
apply HN.
apply le_trans  with n.
apply Hn.
apply sincr_ge_id.
apply pr.
Qed.

Lemma odd_or_even : forall n : nat, exists p : nat, (n = 2*p \/  n = S (2*p)) %nat.
Proof.
intros.
induction n.
exists 0%nat.
left.
trivial.
destruct IHn.
case H; intro.
exists x.
right.
rewrite H0.
reflexivity.
exists (S x).
left.
rewrite H0.
omega.
Qed.

(** a seqence converges if its odd and even subsequences converges to the same limit*)
Lemma even_odd_cv : forall (An : nat -> R) (l : R),
    Un_cv (fun n => An ((2*n) %nat)) l ->  Un_cv (fun n => An (S (2*n) %nat)) l ->
        Un_cv An l.
Proof.
unfold Un_cv.
intros An l Hcve Hcvo eps Heps.
destruct (Hcve eps Heps) as (Ne, He).
destruct (Hcvo eps Heps) as (No, Ho).
exists (max (2*Ne) (S (2*No))).
intros n Hn.
destruct (odd_or_even n) as (p, Hp).
destruct Hp.
rewrite H.
apply He.
apply le_double.
rewrite <- H.
apply le_trans with (max (2 * Ne) (S (2 * No) )).
apply le_max_l.
apply Hn.
rewrite H.
apply Ho.
apply le_double.
apply le_S_n.
rewrite <- H.
apply le_trans with (max (2 * Ne) (S (2 * No))).
apply le_max_r.
apply Hn.
Qed.

Lemma sub_seq_ub_compat : forall (An : nat -> R) (f : nat -> nat) (pr : strictly_increasing f),
    has_ub An -> has_ub (sub_seq An f pr).
Proof.
intros An f pr Hub.
destruct Hub as (m, Hm).
exists m.
intros x Hx.
destruct Hx as (n, Hn).
rewrite Hn.
apply Hm.
exists (f n).
reflexivity.
Qed.

(*?*)
Lemma sub_seq_lb_compat : forall (An : nat -> R) (f : nat -> nat) (pr : strictly_increasing f),
    has_lb An -> has_lb (sub_seq An f pr).
Proof.
intros An f pr Hlb.
destruct Hlb as (m, Hm).
exists m.
intros x Hx.
destruct Hx as (n, Hn).
rewrite Hn.
apply Hm.
exists (f n).
reflexivity.
Qed.

author: coqtail

repo: coqtail

save_path: github-repos/coq/coqtail-coqtail


text:
Require Import Coq.Unicode.Utf8 Arith Bool Ring Setoid String.
Require Import Coq.Lists.ListSet.
Require Import Coq.Sets.Powerset.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Coq.Classes.EquivDec.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Logic.Decidable.
Require Import Coq.Structures.Equalities.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Logic.ClassicalFacts.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.ProofIrrelevance.

Open Scope string_scope.

(*lambda calculus*)
Definition var := string.
Definition varset := string -> bool.

Inductive term :=
| Var : var -> term
| App : term -> term -> term
| Abs : var -> term -> term.

Fixpoint free (t : term) : varset :=
match t with
| Var x => (fun v => if string_dec x v then true else false)
| App a b => (fun v => free a v || free b v)
| Abs x e => (fun v => if string_dec x v then false else free e v)
end.

(*combinators*)

Eval compute in 0.
Eval compute in (pred 0).

Print le.

Eval compute in 0 < 2.

(*semantics*)
Fixpoint D (n : nat) : Set :=
match n with
| O => option False
| S m => option (D m -> D m)
end.
Definition DBottom {n : nat} : D n :=
match n with
| O => None
| S m => None
end.

Ltac unD0 :=
  match goal with
    [ x : D 0 |- _ ] =>
      (destruct x as [ x | _ ]; try inversion x)
  end.

Theorem D0singleton : forall a : D 0, a = None.
Proof.
  intros.
  unD0.
  tauto.
Qed.

Fixpoint abrI {n : nat} : D n -> D (S n) :=
  match n with
  | O => λ _, None
  | S m => λ d,
      match d with
      | None => None
      | Some f => Some (λ x, abrI (f (abrJ x)))
      end
  end
with abrJ {n : nat} : D (S n) -> D n :=
  match n with
  | O => λ _, None
  | S m => λ d,
      match d with
      | None => None
      | Some f => Some (λ x, abrJ (f (abrI x)))
      end
  end
.

Theorem abrINone : forall {n}, abrI (@DBottom n) = DBottom.
Proof.
  destruct n; simpl; tauto.
Qed.
Theorem abrJNone : forall {n}, abrJ (@DBottom (S n)) = DBottom.
Proof.
  destruct n; simpl; tauto.
Qed.

(*
Fixpoint abrJstar {n m : nat} (d : D n) (p : n >= m) : D m.
Proof.
  unfold ge in *.
  apply le_lt_eq_dec in p.
  destruct p.
  - destruct n.
    * contradict l.
      auto with arith.
    * apply abrJ in d.
      apply (abrJstar n m d).
      auto with arith.
  - subst.
    assumption.
Defined.
*)
Fixpoint abrJstar {n m : nat} (d : D n) (p : n >= m) : D m :=
  match le_lt_eq_dec m n p with
  | left l =>
     match n with
     | 0 =>
         λ (d : D 0) l,
         False_rec (D m) (Nat.nlt_0_r m l)
     | S n0 =>
         λ d l,
         abrJstar (abrJ d) (gt_S_le m n0 l)
     end d l
  | right e => eq_rec_r D d e
  end
.

(*
Fixpoint abrIstar {n m : nat} (d : D n) (p : n <= m) : D m.
Proof.
  apply le_lt_eq_dec in p.
  destruct p.
  - destruct m.
    * contradict l.
      auto with arith.
    * apply abrI.
      apply (abrIstar n m d).
      auto with arith.
  - subst.
    assumption.
Defined.
*)
Fixpoint abrIstar {n m : nat} (d : D n) (p : n <= m) : D m :=
  match le_lt_eq_dec n m p with
  | left l =>
     match m with
     | 0 =>
         λ l,
         False_rec (D 0) (Nat.nlt_0_r n l)
     | S m0 =>
         λ l,
         abrI (abrIstar d (gt_S_le n m0 l))
     end l
  | right e =>
     eq_rec_r (λ n, D n → D m) id e d
  end
.

Theorem abrIstarNone : forall {n m : nat} p, abrIstar (@DBottom n) p = (@DBottom m).
Proof.
  unfold DBottom.
  induction n.
  - induction m; intros.
    * compute.
      tauto.
    * simpl.
      rewrite IHm.
      destruct m; simpl; tauto.
  - induction m; intros.
    * contradict p.
      auto with arith.
    * simpl.
      destruct (le_lt_eq_dec (S n) (S m) p).
      + rewrite IHm.
        destruct m; simpl; tauto.
      + inversion e.
        subst.
        assert (e = eq_refl).
        apply proof_irrelevance.
        subst.
        unfold eq_rec_r.
        simpl.
        compute.
        tauto.
Qed.

Theorem abrJstarNone : forall {n m : nat} p, abrJstar (@DBottom n) p = (@DBottom m).
Proof.
  unfold DBottom.
  induction n.
  - induction m; intros.
    * compute.
      tauto.
    * unfold ge in p.
      contradict p.
      auto with arith.
  - induction m; intros.
    * simpl.
      rewrite (@abrJNone 0).
      specialize (IHn 0). simpl in IHn.
      destruct (gt_le_S 0 (S n) (gt_Sn_O n)).
      + rewrite IHm.
        destruct m; simpl; tauto.
      + inversion e.
        subst.
        assert (e = eq_refl).
        apply proof_irrelevance.
        subst.
        unfold eq_rec_r.
        simpl.
        compute.
        tauto.
Qed.

Definition Dprod := forall n, D n.
Definition DD := { d : Dprod | forall n, abrJ (d (S n)) = d n }.

Definition DDBottom' : Dprod := fun n =>
match n with
| O => None
| S _ => None
end.

(*
Definition DDBottom : DD.
Proof.
  unfold DD.
  econstructor.
  intros.
  instantiate (d := DDBottom').
  unfold DDBottom'.
  destruct n; simpl; tauto.
Qed.
*)
Definition DDBottom : DD :=
exist
  (λ d : Dprod, ∀ n, abrJ (d (S n)) = d n)
  DDBottom'
  (λ n,
   match
     n
     return
       (abrJ None =
        match n return (D n) with
        | 0 => None
        | S n => None
        end)
   with
   | 0 => eq_refl
   | S n0 => eq_refl
   end).

Definition DDisBottom (d : DD) : bool :=
match proj1_sig d 1 with
| None => true
| Some _ => false
end.

Theorem sigEq : forall
  {A : Set}
  {p : A -> Prop}
  (x y : sig p),
  proj1_sig x = proj1_sig y -> x = y.
Proof.
  intros.
  apply Subset.subset_eq.
  assumption.
Qed.

Theorem DDisBottomCorrect : forall d,
  d = DDBottom <-> DDisBottom d = true.
Proof.
  split; intros.
  - subst.
    compute.
    tauto.
  - apply sigEq.
    unfold DDisBottom in H.
    destruct d.
    simpl in *.
    apply functional_extensionality_dep.
    induction x0.
    * simpl.
      destruct (x 0); intuition.
    *specialize (e x0).
     destruct x0.
      + destruct (x 1); intuition.
      + simpl in *.
        rewrite IHx0 in e.
        destruct (x (S (S x0))); try tauto.
        inversion e.
Qed.

(*
Definition abrIinf' {n : nat} (d : D n) : Dprod.
Proof.
  unfold Dprod.
  intros.
  destruct (le_ge_dec n n0).
  - apply (@abrIstar n n0); assumption.
  - apply (@abrJstar n n0); assumption.
Qed.
*)
Definition abrIinf' {n : nat} (d : D n) : Dprod :=
fun m =>
match le_ge_dec n m with
| left l => abrIstar d l
| right g => abrJstar d g
end.

Theorem abrJI : forall {n : nat} (d : D n), abrJ (abrI d) = d.
Proof.
  induction n; intros.
  - unD0.
    simpl.
    tauto.
  - destruct d.
    * simpl.
      apply f_equal.
      apply functional_extensionality.
      intros.
      rewrite IHn.
      rewrite IHn.
      tauto.
    * simpl.
      tauto.
Qed.

Definition abrIinf {n : nat} (d : D n) : DD.
Proof.
  unfold DD.
  econstructor.
  intros.
  instantiate (d := abrIinf' d).
  unfold abrIinf'.
  destruct (le_ge_dec n n0);
  destruct (le_ge_dec n (S n0)).
  - simpl.
    destruct (le_lt_eq_dec n (S n0) l0).
    * rewrite abrJI.
      apply f_equal2; try tauto.
      apply proof_irrelevance.
    * subst.
      contradict l.
      auto with arith.
  - contradict l.
    auto with arith.
  - simpl.
    destruct (le_lt_eq_dec n (S n0) l).
    * rewrite abrJI.
      simpl.
      destruct n.
      + unD0.
        simpl.
      .
      apply f_equal2; try tauto.
      apply proof_irrelevance.
    * subst.
      contradict l.
      auto with arith.

      inversion l.
      + .
      Check Streicher_K.
      destruct (gt_S_le n n0 l1).
      Check le_n.
      specialize prop_extensionality.
      eapply prop_extensionality.
      apply proof_irrelevance. le_n.
      auto with arith.
  - Check ?d.
    apply (@abrIstar n n0); assumption.
  - apply (@abrJstar n n0); assumption.
Qed.

(*
Definition abrIinf {n : nat} (d : D n) : DD.
Proof.
  unfold DD.
  intros.
  destruct (le_ge_dec n n0).
  - apply (@abrIstar n n0); assumption.
  - apply (@abrJstar n n0); assumption.
Qed.
*)

Definition abrII (d : DD) : option (DD -> DD).
Proof.
  unfold DD in *.
  intros.
  specialize (d n).
  assumption.
Defined.
(* destruct n.
  - auto.
  - constructor.

  apply Just.*)

Definition abrJJ (d : DD) : DD.
Proof.
  unfold DD in *.
  intros.

author: olydis

repo: CoqExperiments

save_path: github-repos/coq/olydis-CoqExperiments


text:
Require Import Coq.Init.Prelude.

Axiom incr_Some : option nat -> option nat.
Axiom eqn : forall n, incr_Some (Some n) = Some (S n).

Fixpoint pln (n : nat) : option nat :=
  match n with
  | O => Some O
  | S n => incr_Some (pln n)
  end.

Goal pln 1000 = Some 1000.
  Time cbv [pln]. Time repeat rewrite eqn. Time reflexivity. Time Qed.
(*
Finished transaction in 0. secs (0.u,0.s) (successful)
Finished transaction in 21.264 secs (21.133u,0.049s) (successful)
Finished transaction in 0.003 secs (0.003u,0.s) (successful)
Finished transaction in 6.073 secs (6.047u,0.006s) (successful)
*)

author: andres-erbsen

repo: coq-experiments


text:
(**  **)

(*** param_comp: compares old parametricity version with the new one ***)

Load param_unary.

(** lifts everything after n **)
(** morally identity **)
(** LEGACY code for comparison **)
Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term :=
  match t with
  | tRel k => if n <= k then tRel (2*k-n+1) else t
  | tEvar k ts => tEvar k (map (tsl_rec0 n) ts)
  | tCast t c a => tCast (tsl_rec0 n t) c (tsl_rec0 n a)
  | tProd na A B => tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
  | tLambda na A t => tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
  | tLetIn na t A u => tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
  | tApp t lu => tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
  | tCase ik t u br => tCase ik (tsl_rec0 n t) (tsl_rec0 n u)
                            (map (fun x => (fst x, tsl_rec0 n (snd x))) br)
  | tProj p t => tProj p (tsl_rec0 n t)
  | _ => t
  end.

(** LEGACY code for comparison **)
Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
  let tsl_rec1 := tsl_rec1_app None in
  let debug case symbol :=
      debug_term ("tsl_rec1: " ^ case ^ " " ^ symbol ^ " not found") in
  match t with
  | tLambda na A t =>
    let A0 := tsl_rec0 0 A in
    let A1 := tsl_rec1_app None E A in
    tLambda na A0 (tLambda (tsl_name tsl_ident na)
                           (subst_app (lift0 1 A1) [tRel 0])
                           (tsl_rec1_app (option_map (lift 2 2) app) E t))
  | t => let t1 :=
  match t with
  | tRel k => tRel (2 * k)
  | tSort s => tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))

  | tProd na A B =>
    let A0 := tsl_rec0 0 A in
    let A1 := tsl_rec1 E A in
    let B0 := tsl_rec0 1 B in
    let B1 := tsl_rec1 E B in
    let ΠAB0 := tProd na A0 B0 in
    tLambda (nNamed "f") ΠAB0
      (tProd na (lift0 1 A0)
             (tProd (tsl_name tsl_ident na)
                    (subst_app (lift0 2 A1) [tRel 0])
                    (subst_app (lift 1 2 B1)
                               [tApp (tRel 2) [tRel 1]])))
  | tApp t us =>
    let us' := concat (map (fun v => [tsl_rec0 0 v; tsl_rec1 E v]) us) in
    mkApps (tsl_rec1 E t) us'

  | tLetIn na t A u =>
    let t0 := tsl_rec0 0 t in
    let t1 := tsl_rec1 E t in
    let A0 := tsl_rec0 0 A in
    let A1 := tsl_rec1 E A in
    let u0 := tsl_rec0 0 u in
    let u1 := tsl_rec1 E u in
    tLetIn na t0 A0 (tLetIn (tsl_name tsl_ident na) (lift0 1 t1)
                            (subst_app (lift0 1 A1) [tRel 0]) u1)

  | tCast t c A => let t0 := tsl_rec0 0 t in
                  let t1 := tsl_rec1 E t in
                  let A0 := tsl_rec0 0 A in
                  let A1 := tsl_rec1 E A in
                  tCast t1 c (mkApps A1 [tCast t0 c A0]) (* apply_subst ? *)

  | tConst s univs =>
    match lookup_tsl_table E (ConstRef s) with
    | Some t => t
    | None => debug "tConst" (string_of_kername s)
    end
  | tInd i univs =>
    match lookup_tsl_table E (IndRef i) with
    | Some t => t
    | None => debug "tInd" (match i with mkInd s _ => string_of_kername s end)
    end
  | tConstruct i n univs =>
    match lookup_tsl_table E (ConstructRef i n) with
    | Some t => t
    | None => debug "tConstruct" (match i with mkInd s _ => string_of_kername s end)
    end
  | tCase ik t u brs as case =>
    let brs' := List.map (on_snd (lift0 1)) brs in
    let case1 := tCase ik (lift0 1 t) (tRel 0) brs' in
    match lookup_tsl_table E (IndRef (fst ik)) with
    | Some (tInd i _univ) =>
      tCase (i, (snd ik) * 2)%nat
            (tsl_rec1_app (Some (tsl_rec0 0 case1)) E t)
            (tsl_rec1 E u)
            (map (on_snd (tsl_rec1 E)) brs)
    | _ => debug "tCase" (match (fst ik) with mkInd s _ => string_of_kername s end)
    end
  | tProj _ _ => todo "tsl"
  | tFix _ _ | tCoFix _ _ => todo "tsl"
  | tVar _ | tEvar _ _ => todo "tsl"
  | tLambda _ _ _ => tVar "impossible"
  end in
  match app with Some t' => mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
               | None => t1 end
  end.

Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  ((tProd (nNamed "y") (tVar "Y") (tRel 0)))
  ).
Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  ((tProd (nNamed "y") (tVar "Y") (tRel 1)))
  ).
Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  (tProd (nNamed "x") (tRel 0) (tProd (nNamed "y") (tRel 1) (tRel 0)))
  ).
Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  (tProd (nNamed "x") (tRel 0) (tProd (nNamed "y") (tRel 1) (tRel 1)))
  ).

Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  (tProd (nNamed "x") (tVar "X") (tProd (nNamed "y") (tVar "Y") (tRel 0)))
  ).
Compute (tsl_rec1' false (fun n => n) (fun n => n) []
  (tProd (nNamed "x") (tVar "X") (tProd (nNamed "y") (tVar "Y") (tRel 1)))
  ).

Definition tsl_rec1_org := tsl_rec1_app None.

Load de_bruijn_print.
Definition pretty_print := print_term (empty_ext []) [] true.

From MetaCoq Require Import Checker.

Ltac testTerm test :=
let testᵗ := constr:(tsl_rec1'
  false
  (fun n => S(2*n))
  (fun n => 2*n)%nat
  [] test) in
let testᵗp := constr:(tsl_rec1'
  true
  (fun n => S(2*n))
  (fun n => 2*n)%nat
  [] test) in
let testᵗ2 := constr:(tsl_rec1_org [] test) in
run_template_program (
    print_nf test;;
    bruijn_print test;;
    bruijn_print testᵗ;;
    bruijn_print testᵗ2;;
    bruijn_print testᵗp) (fun _ =>
let eq := eval hnf in (eq_term init_graph testᵗ testᵗ2) in
idtac "";idtac "equal: " eq;idtac "=====================";idtac ""
).

Ltac testTerms xs :=
    lazymatch xs with
    | [] => idtac "finished"
    | ?x::?xs => testTerm x;testTerms xs
    end.

Compute (ltac:(testTerms [
(tRel 0); (** test base term **)
(tProd nAnon (tRel 0) (tRel 1)); (** translation outside the scope **)
(** (tProd nAnon (tVar "None") (tProd nAnon (tVar "None") (tProd nAnon (tRel 0) (tRel 1)))); **) (** todo tsl is not printable **)
<% forall (A:Type), forall (a:A), Type %>; (** dependent prods and type translation application **)
<% forall (A:Type), forall (a:nat), Type %>; (** prod with constants **)
<% forall (f:nat -> Type) (n:nat), f n %>; (** application and body translation **)
<% forall (T:Type), Type %>; (** type translation **)
<% fun (P:Type->Type) => fun (Q:Type) => P Q %>; (** lambda with applications **)
<% fun (P:Type) => forall (p:P), P %>; (** access of outer binder **)
<% fun (P:Type) => forall (p:P) (q:P), P %>; (** multiple arguments **)
<% fun (P:Type) (Q:Type) => forall (p:P), P %>; (** multiple lambdas **)
<% fun (P:Type->Type) => fun (Q:Type) => forall (X:P Q), forall (q:Q), P Q %>; (** application and interleaved binder **)
<% fun (P:Type) => let X := P in let Y := X in forall (Q:Type->Type->Type), Q Y X %>; (** complex let in test **)
<% Type %>
])).

(** equal: true for all **)

(** takes 2min 30s with eq_term **)

author: uds-psl