rewrule.v

Symbol pplus : nat -> nat -> nat.
Notation "a ++ b" := (pplus a b).

Rewrite Rules plus_rew := ?n ++ 0 ==> ?n
with ?n ++ S ?n' ==> S (?n ++ ?n')
with 0 ++ ?n ==> ?n
with S ?n ++ ?n' ==> S (?n ++ ?n').

Check eq_refl : 5 ++ 10 = 15.
Check (fun _ _ => eq_refl) : forall n n', 2 + n ++ 3 + n' = 5 + (n ++ n').
Check (fun _ _ _ => eq_refl) : forall n n' n'', 2 + n ++ 1 + n' ++ 2 + n'' = 5 + (n ++ n' ++ n'').

#[unfold_fix] Symbol raise : forall P: Type, P.

Rewrite Rules raise_rew :=
  match raise bool as b return ?P with
    true => _ | false => _
  end ==> raise (?P@{b := raise bool})

with
  match raise nat as n return ?P with
    0 => ?p | S n => ?p'
  end ==> raise (?P@{n := raise nat}).

Check eq_refl : match raise bool as b return true = b with true => eq_refl | false => raise _ end = raise (true = raise bool).

Check eq_refl : match raise bool as b return b = b with true | false => eq_refl end = raise (raise bool = raise bool).

Check (fun _ => eq_refl) : forall n, raise nat + n = raise nat.


Rewrite Rule plus_assoc := ?n ++ ?m ++ ?p ==> (?n ++ ?m) ++ ?p.

From Coq Require Import ssreflect.

Lemma add_comm m n : m ++ n = n ++ m.
Proof.
  induction n; cbn; auto.
Qed.

Inductive vector {A : Type} | : nat -> Type :=
| vnil : vector 0
| vcons {n} : A -> vector n -> vector (S n).
Arguments vector : clear implicits.


Symbol vapp : forall {A n m}, vector A n -> vector A m -> vector A (n ++ m).
Arguments vapp {_ _ _}.

Rewrite Rules vapp_rew := vapp (m := 0) ?v _ ==> ?v
with vapp (n := 0) _ ?v' ==> ?v'
with @vapp ?A (S ?n) ?m (vcons ?a ?v) ?v' ==> @vcons ?A _ ?a (@vapp ?A ?n ?m ?v ?v').

Fixpoint vapp' {A n m} (v : vector A n) (v' : vector A m) : vector A (n ++ m) :=
  match v with
  | vnil => v'
  | vcons a v => vcons a (vapp' v v')
  end.

Lemma vapp'_vapp {A n m} (v : vector A n) (v' : vector A m) : vapp' v v' = vapp v v'.
Proof.
  induction v => //=.
  now f_equal.
Qed.

Lemma vapp_nil {A n} (v : vector A 0) (v' : vector A n) : vapp v v' = v'.
Proof.
  reflexivity.
Qed.

Lemma vapp_nil_r {A n} (v : vector A n) (v' : vector A 0) : vapp v v' = v.
Proof.
  cbn.
  refine (match v' with vnil => _ end).
  induction v => //=.
Qed.

Lemma vapp_assoc {A n m p} (v : vector A n) (v' : vector A m) (v'' : vector A p) :
  vapp v (vapp v' v'') = vapp (vapp v v') v''.
Proof.
  induction v => //. idtac => /=. idtac => /=.
  now f_equal.
Qed.

Definition vhead {A n} (v : vector A (S n)) : A :=
  match v with vcons a _ => a end.

Lemma vheadapp {A n m} (v : vector A (S n)) (v' : vector A m) : vhead (vapp v v') = vhead v.
  refine (
    match v in vector _ (S n) return vhead (vapp v v') = vhead v with vcons a v => _ end
  ).
  reflexivity.
Qed.

Fixpoint vtail_default {A} a {n} (v : vector A n) := match v with vnil => a | vcons a v => vtail_default a v end.

Definition vtail {A n} (v : vector A (S n)) : A :=
  match v with
  | vcons a v => vtail_default a v
  end.

Lemma vtail_vtail_default {A n} (v : vector A (S n)) a : vtail_default a v = vtail v.
Proof.
  refine (match v in vector _ (S n) with vcons a v => _ end).
  reflexivity.
Qed.

Lemma vtailapp {A n m} (v : vector A n) (v' : vector A (S m)) : vtail (n := n ++ m) (vapp v v') = vtail v'.
Proof.
  induction v => //=.
  erewrite <- vtail_vtail_default in IHv.
  apply IHv.
Qed.


Symbol err : forall P: Type, P.
Symbol unk : forall P: Type, P.
Symbol cast : forall A B, A -> B.
Notation "<< B <== A >> t" := (cast A B t) (at level 10).

(* Examples of rewrite rules where the order in which variables are introduced must match the order in which they are used. The order must match the original definition, ignoring notations. *)
Rewrite Rule r1 := (<< ?B <== ?A >> _) ==> (unk ?B).
Rewrite Rule r2 := cast ?A ?B _ ==> (unk ?B).

(* These work OK *)
Rewrite Rule r3 := (<< ?B <== ?A >> ?t) ==> (unk ?B).
Rewrite Rule r4 := cast ?A ?B ?t ==> (unk ?B).

Rewrite Rule r5 := cast nat bool (unk nat) ==> err bool.

Rewrite Rule r6 := unk (forall (x : ?A), ?B) ==> fun (x : ?A) => unk ?B.

Rewrite Rule r7 := << forall (y : ?C), ?D <== forall (x: ?A), ?B >> ?f ==> fun (y : ?C) => let x := << _ <== _ >> y in << ?D <== ?B@{x := x} >> (?f x).


(* Type (Set) is not a valid pattern for symbol application *)
Rewrite Rule r8 := cast Type Type ?t ==> ?t.


Symbol brk : bool -> bool -> bool.
Rewrite Rules brk_rew := brk true ?b ==> true
with brk ?b true ==> false.

Lemma f0 : False.
  cut { b | brk true b = brk b true}.
  2: exists true; reflexivity.
  intros [b H].
  cbn in H.
  discriminate.
Qed.


Definition f b (H : brk true b = brk b true) : False :=
  eq_ind true (fun e => if e then True else False) I false H.

Eval lazy in (f true eq_refl). (* = I : False *)


Universe u.
Symbol id@{i} : Type@{i} -> Type@{u}.

Rewrite Rule id_id := id ?t ==> ?t.


Definition U : Type@{u} := id Type@{u}.
Check U : U.

Definition id'@{i} : Type@{i} -> Type@{u} := fun (t: Type@{i}) => t.
Fail Definition U' : Type@{u} := id' Type@{u}.

Require Import Coq.Logic.Hurkens.
Check TypeNeqSmallType.paradox U eq_refl : False.