(** Lesson 1 -- What changes when an equation computes? (~25 minutes.)

    Run [python3 check.py] from this folder, then visit the L*.v files
    in order. README.md explains editor setup. All examples use Corelib.

    We start with ordinary addition, then declare a fresh symbol whose
    rules compute on either argument. Before each [Fail] or [Eval],
    predict what Rocq will do. No theorem about the whole rewrite system
    is being claimed by these individual examples.
*)

From Corelib Require Import Init.Nat.

Set Guard Checking.
Set Universe Checking.
Test Guard Checking.
Guard Checking is on
Test Universe Checking.
Universe Checking is on

(** Ordinary addition inspects its FIRST argument. A variable blocks
    that match, even when the second argument is zero. *)
Print Nat.add.
add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat

Arguments add (n m)%_nat_scope
Eval cbn in (fun n => 0 + n).
= fun n : nat => n
: nat -> nat
Eval cbn in (fun n => n + 0).
= fun n : nat => n + 0
: nat -> nat

Definition ordinary_left_zero : forall n, 0 + n = n :=
  fun n => eq_refl.

Fail Definition ordinary_right_zero_by_conversion : forall n, n + 0 = n :=
  fun n => eq_refl.
The command has indeed failed with message:
In environment
n : nat
The term "eq_refl" has type "n + 0 = n + 0" while it is expected to have type
 "n + 0 = n"
(cannot unify "n + 0" and "n").

(** The missing computational equation is still PROVABLE. Hide this
    proof and try it yourself: what is the induction hypothesis? *)
Lemma ordinary_right_zero : forall n, n + 0 = n.
forall n : nat, n + 0 = n
Proof.
forall n : nat, n + 0 = n
  induction n as [|n IH].
0 + 0 = 0
n: nat
IH: n + 0 = n
S n + 0 = S n
  -
0 + 0 = 0 reflexivity.
  -
n: nat
IH: n + 0 = n
S n + 0 = S n cbn.
n: nat
IH: n + 0 = n
S (n + 0) = S n rewrite IH.
n: nat
IH: n + 0 = n
S n = S n reflexivity.
Qed.

(** [rewrite] uses an equality proof to transform a goal. It does not
    install a native rule for [Nat.add]. *)
Example ordinary_use (n : nat) : S (n + 0) = S n.
n: nat
S (n + 0) = S n
Proof.
n: nat
S (n + 0) = S n rewrite ordinary_right_zero.
n: nat
S n = S n reflexivity. Qed.

Fail Definition ordinary_still_stuck : forall n, n + 0 = n :=
  fun n => eq_refl.
The command has indeed failed with message:
In environment
n : nat
The term "eq_refl" has type "n + 0 = n + 0" while it is expected to have type
 "n + 0 = n"
(cannot unify "n + 0" and "n").

(** A Symbol has a declared type and no defining body. This declaration
    is an assumption about a new operation; it is not a Fixpoint. *)
Symbol pplus : nat -> nat -> nat.
Check pplus.
pplus
     : nat -> nat -> nat
Print pplus.
*** [ pplus : nat -> nat -> nat ]

Arguments pplus (_ _)%_nat_scope

Fail Definition before_rules : forall n, pplus n 0 = n :=
  fun n => eq_refl.
The command has indeed failed with message:
In environment
n : nat
The term "eq_refl" has type "pplus n 0 = pplus n 0"
while it is expected to have type "pplus n 0 = n" (cannot unify 
"pplus n 0" and "n").

(** Parallel addition, following the native rewrite-rule manual.
    [?n] binds a pattern variable. The same name on the right refers to
    the matched term. Rules here overlap: overlap is not itself failure
    of confluence. That distinction will matter in Lesson 5. *)
Rewrite Rule pplus_rules :=
| pplus ?n 0 => ?n
| pplus ?n (S ?m) => S (pplus ?n ?m)
| pplus 0 ?n => ?n
| pplus (S ?n) ?m => S (pplus ?n ?m).

Definition native_right_zero : forall n, pplus n 0 = n :=
  fun n => eq_refl.
Definition native_left_zero : forall n, pplus 0 n = n :=
  fun n => eq_refl.
Definition native_successors :
  forall n m, pplus (S n) (S m) = S (S (pplus n m)) :=
  fun n m => eq_refl.

Eval cbn in (fun n => pplus n 0).
= fun n : nat => n
: nat -> nat
Eval cbn in (fun n m => pplus (S n) (S m)).
= fun n m : nat => S (S (pplus n m))
: nat -> nat -> nat
Example concrete_sum : pplus 5 10 = 15.
pplus 5 10 = 15
Proof.
pplus 5 10 = 15 reflexivity. Qed.

(** Conversion also aligns TYPES. [P] is an arbitrary family indexed
    by natural numbers. Inspect the body: there is no equality transport
    in it. The expected and actual types become equal by computation. *)
Definition native_reindex (P : nat -> Type) (n : nat)
  (x : P (pplus n 0)) : P n := x.

Fail Definition ordinary_reindex (P : nat -> Type) (n : nat)
  (x : P (n + 0)) : P n := x.
The command has indeed failed with message:
In environment
P : nat -> Type
n : nat
x : P (n + 0)
The term "x" has type "P (n + 0)" while it is expected to have type "P n".

Print native_right_zero.
native_right_zero =
fun n : nat => eq_refl
     : forall n : nat, pplus n 0 = n

Arguments native_right_zero n%_nat_scope
Print native_reindex.
native_reindex =
fun (P : nat -> Type) (n : nat) (x : P (pplus n 0)) => x
     : forall (P : nat -> Type) (n : nat), P (pplus n 0) -> P n

Arguments native_reindex P%_function_scope n%_nat_scope x
Print Assumptions ordinary_right_zero.
Theory:
Rewrite rules are allowed (subject reduction might be broken)
Print Assumptions native_right_zero.
Axioms:
pplus : nat -> nat -> nat
Theory:
Rewrite rules are allowed (subject reduction might be broken)

(** Checkpoint

    1. Why can [eq_refl] prove [native_right_zero]?
    2. Did proving [ordinary_right_zero] change computation of [Nat.add]?
    3. Which assumption and theory flag appear for the native example?
    4. Does one successful equality prove confluence or termination?

    Cues: conversion uses the registered rule; an equality theorem does
    not change native reduction; the symbol [pplus] and rewrite opt-in
    are reported; testing equalities establishes those examples only.

    Next: L02_Patterns.v -- which declarations are actually rejected?
*)