CODEWITHSUNDEEP
coq
First Last
First Last

Reputation: 33

Reduction of terms with fix. (Coq)

The function 'f' appeared in my proof. I need to show that it is equal to zero when both its arguements are the same numbers. In fact, function f is equivalent to "greater or equal to" function "geq".

I am using https://github.com/HoTT/HoTT library, but it is clear that problem is not library-specific, so I made a self-contained example below. It should be runnable with Coq v8.5 at least. Part of code from library:

Local Set Typeclasses Strict Resolution.
Local Unset Elimination Schemes.
Global Set Keyed Unification.
Global Unset Refine Instance Mode.
Global Unset Strict Universe Declaration.
Global Unset Universe Minimization ToSet.
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Scheme paths_ind := Induction for paths Sort Type.
Arguments paths_ind [A] a P f y p.
Scheme paths_rec := Minimality for paths Sort Type.
Arguments paths_rec [A] a P f y p.
Definition paths_rect := paths_ind.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope. 

Inductive Bool := true | false.

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end.

Main part:

Definition code_n := (fix code_n (m n : nat) {struct m} : Bool :=
       match m with
       | 0 =>
           match n with
           | 0 => true
           | S n' =>false 
           end
       | S m' =>
           match n with
           | 0 => false
           | S n' => code_n m' n'
           end
       end).

Definition f (m:nat) := (fix acc (m0 : nat) : nat :=
   match m0 with
   | 0 => 0
   | S m1 => add (if code_n m1 m then 1 else 0) (acc m1)
   end).

Eval compute in f 1 1. (*=0*)
Eval compute in f 1 2. (*=1*)
Eval compute in f 2 2. (*=0*)
Fixpoint impprf (m:nat): f m m = 0. (*How to prove it??*)

As a first step, it is easy to show that code_n is true when both its arguments are equal:

Fixpoint code_n_eq (v : nat): (code_n v v) = true 
:= match v as n return (code_n n n = true) with
   | 0 => @idpath Bool true
   | S v0 => code_n_eq v0
   end.

Second step: problem may be reformulated as proving that 

code_n_eq (S m) (S m) = code_n_eq m m.

or, maybe, that 

(0 = code_n_eq m m)-> (0 =  code_n_eq (S m) (S m) ).

Upvotes: 2

Views: 1127

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

To make proving easier I had to replace your custom definitions with their standard analogues and I've taken some liberty to rearrange the code. You can revert the changes and see that everything will still work, provided that you use bool instead of Bool and + instead of your add.

Fixpoint code_n (m n : nat) {struct m} : bool :=
  match m, n with
  | 0, 0 => true
  | 0, S _ | S _, 0 => false
  | S m', S n' => code_n m' n'
  end.

Fixpoint f (m n :nat) : nat :=
  match n with
  | 0 => 0
  | S n' => (if code_n n' m then 1 else 0) + (f m n')
  end.

In what follows I'm using some proof automation to show the main idea and not to get bogged down in details. Frequently, when we're trying to prove a lemma by induction, it's easier (it even may be the only way) to prove a stronger statement first.

Require Import Omega.  (* to use `omega` magical tactic *)

Lemma code_n_eq m n :
  (code_n m n) = true <-> m = n.
Proof.
  revert n; induction m; destruct n; try easy; firstorder.
Qed.

(* generalize what we want to prove *)
Lemma gte m n :
  m >= n -> f m n = 0.
Proof.
  revert m; induction n; destruct m; try easy; firstorder.
  simpl. destruct (code_n n (S m)) eqn:E.
  - apply code_n_eq in E; omega.
  - assert (m >= n); firstorder.
Qed.

Lemma impprf (m:nat): f m m = 0.
Proof. apply gte. auto. Qed.

Upvotes: 4

Related Questions