Scheme Equality for nat.

Inductive mul3 : nat -> Prop :=
  | T0 : mul3 0
  | T3: forall n, mul3 n -> mul3 (3 + n).

Lemma inv_mul_3plusn : forall n, mul3 (3 + n) -> mul3 n.
Proof.
intros n m. 
exact 
(  let diag x := match x with S (S (S y)) => y | _ => 3 + n end in
       match m in (mul3 n0) return mul3 (diag n0) with
       | T0 => m
       | T3 _ m0 => m0
       end
).
(*
pose (diag x := match x with S (S (S y)) => y | _ => 3 + n end).
change (mul3 (diag (3 + n))). case m.
  exact m.
  unfold diag; simpl. clear diag n m. intros n m; exact m.  
*)
Qed.

(* Not in the paper: version without 0 *)
Lemma inv_mul_3plusn_no0 : forall n, mul3 (3 + n) -> mul3 n.
Proof.
intros n m.
pose (diag x := match x with | S (S (S y)) => mul3 y | _ => mul3 (3+n) end).
change (diag (3 + n)). case m.
  simpl. exact m.
  unfold diag; simpl. clear diag n m. intros n m; exact m.  
(*
       let diag x := match x with S (S (S y)) => mul3 y | _ => mul3 (3+n) end in
       match m in (mul3 n0) return (diag n0) with
       | T0 => m
       | T3 _ m0 => m0
       end
*)
Qed.

(* With inversion for comparison *)
Lemma inv_mul_3plusn_inv : forall n, mul3 (3 + n) -> mul3 n.
Proof.
intros n m. inversion_clear m. assumption.
(*
Proof: fun (n : nat) (m : mul3 (3 + n)) =>
       let H :=
         match m in (mul3 n0) return (n0 = 3 + n -> mul3 n) with
         | T0 =>
             fun H : 0 = 3 + n =>
             (fun H0 : 0 = 3 + n =>
              let H1 :=
                eq_ind 0
                  (fun e : nat => match e with
                                  | 0 => True
                                  | S _ => False
                                  end) I (3 + n) H0 in
              (fun H2 : False => False_ind (mul3 n) H2) H1) H
         | T3 n0 H =>
             fun H0 : 3 + n0 = 3 + n =>
             let H1 :=
               (fun H1 : 3 + n0 = 3 + n =>
                let H2 :=
                  f_equal
                    (fun e : nat =>
                     match e with
                     | 0 => n0
                     | 1 => n0
                     | 2 => n0
                     | S (S (S n3)) => n3
                     end) H1 in
                (fun H3 : n0 = n =>
                 eq_ind n (fun n1 : nat => mul3 n1 -> mul3 n)
                   (fun H4 : mul3 n => H4) n0 (sym_eq H3)) H2) H0 in
             H1 H
         end in
       H (refl_equal (3 + n))
*)
Qed.

(* ----------------------------------------------------------------------- *)

Section sec_absu_2ismul3.

Variable C: Prop.

Lemma absurd2_inv : mul3 2 -> C.
Proof.
intros H. inversion_clear H.
(*
Proof: fun H : mul3 2 =>
       let H0 :=
         match H in (mul3 n) return (n = 2 -> C) with
         | T0 =>
             fun H0 : 0 = 2 =>
             (fun H1 : 0 = 2 =>
              let H2 :=
                eq_ind 0
                  (fun e : nat => match e with
                                  | 0 => True
                                  | S _ => False
                                  end) I 2 H1 in
              (fun H3 : False => False_ind C H3) H2) H0
         | T3 n H0 =>
             fun H1 : 3 + n = 2 =>
             let H2 :=
               (fun H2 : 3 + n = 2 =>
                let H3 :=
                  eq_ind (3 + n)
                    (fun e : nat =>
                     match e with
                     | 0 => False
                     | 1 => False
                     | 2 => False
                     | S (S (S _)) => True
                     end) I 2 H2 in
                (fun H4 : False => False_ind (mul3 n -> C) H4) H3) H1 in
             H2 H0
         end in
       H0 (refl_equal 2)
*)
Qed.


Lemma absurd2_interact : mul3 2 -> C.
Proof.
intros m.
pose (diag x := match x with 2 => C | _ => True end). 
change (diag 2). case m; clear m.
  simpl. exact I.
  simpl. intros; exact I.  
Qed.

Definition absurd2_prog : mul3 2 -> C :=
  fun H =>
  let diag x := match x with 2 => C | _ => True end in
    match H in (mul3 n) return (diag n) with
      | T0 => I
      | T3 _ _ => I
    end.

Definition absurd2_prog_pure : mul3 2 -> C :=
  fun H =>
  let diag x := match x with 2 => C | _ => mul3 2 end in
    match H in (mul3 n) return (diag n) with
      | T0 => H
      | T3 _ _ => H
    end.

End sec_absu_2ismul3.

(* ----------------------------------------------------------------------- *)
(* Variant without strong elimination *)

(*Notation "+3 n" := (S (S (S n))) (at level 10).*)

(* *)

Lemma invmul10 : mul3 10 -> 0 = 1.
Proof.
intro m.
pose (diag x := if nat_beq x 10 then 1 else 0).
change (0 = diag 10).
case m; clear m; reflexivity || intros n m.
repeat (case m; clear m n; reflexivity || intros n m).
Qed.

Definition invmul10_prog : mul3 10 -> 0 = 1 := 
fun m : mul3 10 =>
let diag x := if nat_beq x 10 then 1 else 0 in
match m in (mul3 n) return (0 = diag n) with
| T0 => refl_equal (diag 0)
| T3 _ m0 =>
    match m0 in (mul3 n0) return (0 = diag (3 + n0)) with
    | T0 => refl_equal (diag (3 + 0))
    | T3 _ m1 =>
        match m1 in (mul3 n1) return (0 = diag (3 + (3 + n1))) with
        | T0 => refl_equal (diag (3 + (3 + 0)))
        | T3 _ m2 =>
            match
              m2 in (mul3 n2) return (0 = diag (3 + (3 + (3 + n2))))
            with
            | T0 => refl_equal (diag (3 + (3 + (3 + 0))))
            | T3 n2 _ => refl_equal (diag (3 + (3 + (3 + (3 + n2)))))
            end
        end
    end
end.

(* ----------------------------------------------------------------------- *)
(* Non deterministic relation with exponential blow-up *)

Inductive nd (f g: nat-> nat) (c: nat) : nat -> Prop :=
  | Nc: nd f g c c
  | Nf: forall n, nd f g c n -> nd f g c (f n)
  | Ng: forall n, nd f g c n -> nd f g c (g n).

(* *)

Definition pl3 n := 3 + n.
Definition pl5 n := 5 + n.

(* *)

Lemma absurd_nd4_inv : forall C: Prop, nd pl3 pl5 7 4 -> C.
Proof.
intros C H. inversion_clear H. inversion_clear H0. 
Qed.
(* proof term : 102 lines *)

Lemma absurd_nd4_interac : forall C: Prop, nd pl3 pl5 7 4 -> C.
Proof.
intros C H.
pose (diag x := match x with 4 => C | _ => nd pl3 pl5 7 4 end).
change (diag 4). 
case H; (intros; exact H) || (intros n N; case N; intros; exact H).
Qed.

Definition absurd_nd4_prog : forall C: Prop, nd pl3 pl5 7 4 -> C :=
  fun C H => 
    let diag x := match x with 4 => C | _ => nd pl3 pl5 7 4 end in
    match H in (nd _ _ _ n) return diag n with
      | Nf _ N =>
        match N in (nd _ _ _ n) return diag (pl3 n) with
          | Nc => H
          | _ => H
        end
      | _ => H
    end.

Definition absurd_nd4_prog_full : forall C: Prop, nd pl3 pl5 7 4 -> C :=
  fun C H => 
    let diag x := match x with 4 => C | _ => nd pl3 pl5 7 4 end in
    match H in (nd _ _ _ n) return diag n with
      | Nc => H
      | Nf _ N =>
        match N in (nd _ _ _ n) return diag (pl3 n) with
          | Nc => H
          | Nf _ _ => H
          | Ng _ _ => H
        end
      | Ng _ _ => H
    end.

(* ----------------------------------------------------------------------- *)

(* *)

Variable p : nat.

Definition tr15 := nd (plus 6) (plus 9) 15.

Lemma tr15_beq : tr15 40 -> tr15 p.
Proof.
intros t40.
pose (diag n := if nat_beq n 40 then p else 40).
change (tr15 (diag 40)).  assert (gen: forall n, tr15 n -> tr15 (diag n)).
  repeat (exact t40 || intros n t; exact t40 || (case t; clear t n)).
  apply gen; exact t40.
Defined.


Lemma tr15_inv : tr15 40 -> tr15 p.
Proof.
intros t40.
inversion_clear t40.
repeat (match goal with [ H : nd _ _ _ _ |-  _ ] => inversion_clear H end).
repeat (match goal with [ H : nd _ _ _ _ |-  _ ] => inversion_clear H end).
Qed.




(* ----------------------------------------------------------------------- *)
(* Programming with dependent types *)

Inductive div3spec: nat -> nat -> Prop :=
  | D0 : div3spec 0 0
  | D3 : forall d n, div3spec d n -> div3spec (S d) (3 + n).

Definition div3Set_inv : forall n, mul3 n -> {t | div3spec t n}.
Proof.
fix 1.
intros n; case n; clear n.
  intro m; exists 0. 
    constructor.
 
    intros n ; case n; clear n.
      intro m; exists 7  (* fake *). 
        inversion m. 

    intros n ; case n; clear n.
      intro m; exists 5  (* fake *). inversion m. 

    intros n m; case (div3Set_inv n).
      inversion_clear m. trivial.
      intros t d3. exists (S t). apply (D3 t n d3). 
Defined.

Definition div3Set_small : forall n, mul3 n -> {t | div3spec t n}.
Proof.
fix 1.
intros n; case n; clear n.
  intro m; exists 0. (*  e : mul3 0 |-  div3spec 0 0 *)
    constructor.
  
    intros n ; case n; clear n.
      intro m; exists 7  (* fake *).  (* m: mul3 1 |-  div3spec 7 1  *)
       pose (diag1 x := if nat_beq x 1 then 7 else 0);
       pose (diag2 x := if nat_beq x 1 then 1 else 0).
       change (div3spec (diag1 1) (diag2 1)). case m; intros; apply D0.
  
    intros n ; case n; clear n.
      intro m; exists 5  (* fake *).  (* m: mul3 2 |-  div3spec 5 1  *)
       pose (diag1 x := if nat_beq x 2 then 5 else 0);
       pose (diag2 x := if nat_beq x 2 then 2 else 0).
       change (div3spec (diag1 2) (diag2 2)). case m; intros; apply D0.

    intros n m; case (div3Set_small n). (* m: mul3 (+3 n) |-  mul3 n *)
      pose (diag x := match x with (S (S (S y))) => y | _ => 3 + n end).
      change (mul3 (diag (S (S (S n))))).  case m; simpl. 
         intros; exact m.
         intros; assumption.
      intros t d3. exists (S t). apply (D3 t n d3). 
Defined.