From 9c2efdde9c4b68e5314c4fb1c0dedcea0d138bb5 Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 25 Oct 2018 16:41:06 +0200
Subject: conversion tactics

---
 examples/Example.v | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

(limited to 'examples')

diff --git a/examples/Example.v b/examples/Example.v
index 8138469..2f3ca73 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -68,3 +68,73 @@ Goal forall b1 b2 x1 x2,
 Proof.
   verit.
 Qed.
+
+
+(* Examples of using the conversion tactics *)
+
+Local Open Scope positive_scope.
+
+Goal forall (f : positive -> positive) (x y : positive),
+  implb ((x + 3) =? y)
+        ((f (x + 3)) <=? (f y))
+  = true.
+Proof.
+pos_convert.
+verit.
+Qed.
+
+Goal forall (f : positive -> positive) (x y : positive),
+  implb ((x + 3) =? y)
+        ((3 <? y) && ((f (x + 3)) <=? (f y)))
+  = true.
+Proof.
+pos_convert.
+verit.
+Qed.
+
+Local Close Scope positive_scope.
+
+Local Open Scope N_scope.
+
+Goal forall (f : N -> N) (x y : N),
+  implb ((x + 3) =? y)
+        ((f (x + 3)) <=? (f y))
+  = true.
+Proof.
+N_convert.
+verit.
+Qed.
+
+Goal forall (f : N -> N) (x y : N),
+  implb ((x + 3) =? y)
+        ((2 <? y) && ((f (x + 3)) <=? (f y)))
+  = true.
+Proof.
+N_convert.
+verit.
+Qed.
+
+Local Close Scope N_scope.
+
+Require Import NPeano.
+Local Open Scope nat_scope.
+
+Goal forall (f : nat -> nat) (x y : nat),
+  implb (Nat.eqb (x + 3) y)
+        ((f (x + 3)) <=? (f y))
+  = true.
+Proof.
+nat_convert.
+verit.
+Qed.
+
+Goal forall (f : nat -> nat) (x y : nat),
+  implb (Nat.eqb (x + 3) y)
+        ((2 <? y) && ((f (x + 3)) <=? (f y)))
+  = true.
+Proof.
+nat_convert.
+verit.
+Qed.
+
+Local Close Scope nat_scope.
\ No newline at end of file
-- 
cgit